1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl
  5  
  6  Infinite sum over a topological monoid
  7  
  8  This sum is known as unconditionally convergent, as it sums to the same value under all possible
  9  permutations. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute
 10  convergence.
 11  
 12  Note: There are summable sequences which are not unconditionally convergent! The other way holds
 13  generally, see `tendsto_sum_nat_of_has_sum`.
 14  
 15  Reference:
 16  * Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups)
 17  
 18  -/
 19  import logic.function algebra.big_operators data.set.lattice data.finset
src         └────────────┘ └───────────────────┘ └──────────────┘ └─────────┘
 20         topology.metric_space.basic topology.algebra.uniform_group topology.algebra.ring
src         └─────────────────────────┘ └────────────────────────────┘ └───────────────────┘
 21         topology.algebra.ordered topology.instances.real
src         └──────────────────────┘ └─────────────────────┘
 22  
 23  noncomputable theory
 24  open lattice finset filter function classical
 25  open_locale topological_space
 26  local attribute [instance] classical.prop_decidable -- TODO: use "open_locale classical"
id                              └──────────────────────┘
src                             └──────────────────────┘
typ                             └──────────────────────┘
 27  
 28  def option.cases_on' {α β} : option α → β → (α → β) → β
id                                └────┘             
src                               └────┘
typ                               └────┘             
 29  | none     n s := n
id     └──┘     
src    └──┘
typ    └──┘     
 30  | (some a) n s := s a
id      └──┘     
src     └──┘
typ     └──┘     
 31  
 32  variables {α : Type*} {β : Type*} {γ : Type*}
 33  
 34  section has_sum
 35  variables [add_comm_monoid α] [topological_space α]
id              └─────────────┘     └───────────────┘
src             └─────────────┘     └───────────────┘
typ             └─────────────┘     └───────────────┘
doc                                 └───────────────┘
 36  
 37  /-- Infinite sum on a topological monoid
 38  The `at_top` filter on `finset α` is the limit of all finite sets towards the entire type. So we sum
 39  up bigger and bigger sets. This sum operation is still invariant under reordering, and a absolute
 40  sum operator.
 41  
 42  This is based on Mario Carneiro's infinite sum in Metamath.
 43  
 44  For the definition or many statements, α does not need to be a topological monoid. We only add
 45  this assumption later, for the lemmas where it is relevant.
 46  -/
 47  def has_sum (f : β → α) (a : α) : Prop := tendsto (λs:finset β, s.sum f) at_top (𝓝 a)
id                                          └─────┘     └────┘   └──┘   └────┘   
src                                            └─────┘     └────┘     └──┘    └────┘  
typ                                         └─────┘     └────┘   └──┘   └────┘   
doc                                            └─────┘     └────┘             └────┘  
 48  
 49  /-- `summable f` means that `f` has some (infinite) sum. Use `tsum` to get the value. -/
 50  def summable (f : β → α) : Prop := ∃a, has_sum f a
id                                     └─────┘  
src                                       └─────┘
typ                                    └─────┘  
doc                                         └─────┘
 51  
 52  /-- `tsum f` is the sum of `f` it exists, or 0 otherwise -/
 53  def tsum (f : β → α) := if h : summable f then classical.some h else 0
id                         └┘     └──────┘       └────────────┘       
src                          └┘     └──────┘        └────────────┘        
typ                        └┘     └──────┘       └────────────┘       
doc                                 └──────┘
 54  
 55  notation `∑` binders `, ` r:(scoped f, tsum f) := r
id                                          └──┘
src                                         └──┘
typ                                         └──┘
doc                                         └──┘
 56  
 57  variables {f g : β → α} {a b : α} {s : finset β}
id                                          └────┘
src                                         └────┘
typ                                         └────┘
doc                                         └────┘
 58  
 59  lemma has_sum_tsum (ha : summable f) : has_sum f (∑b, f b) :=
id                            └──────┘     └─────┘     
src                           └──────┘      └─────┘     
typ                           └──────┘     └─────┘     
doc                           └──────┘      └─────┘     
 60  by simp [ha, tsum]; exact some_spec ha
id            └┘  └──┘         └───────┘ └┘
src     └────┘  └┘└──┘  └────┘└───────┘  
typ     └────┘└┘└┘└──┘  └────┘└───────┘└┘
doc     └────┘  └┘└──┘  └────┘           
txt     └────┘  └┘      └────┘           
par     └────┘  └┘      └────┘           
pid           └┘                      
st     └────────────────────────────────────
 61  
src  
typ  
doc  
txt  
par  
pid  
st   
 62  lemma summable_spec (ha : has_sum f a) : summable f := ⟨a, ha⟩
id                             └─────┘      └──────┘        └┘
src                            └─────┘        └──────┘
typ                            └─────┘      └──────┘        └┘
doc                            └─────┘        └──────┘
 63  
 64  /-- Constant zero function has sum `0` -/
 65  lemma has_sum_zero : has_sum (λb, 0 : β → α) 0 :=
id                        └─────┘            
src                       └─────┘
typ                       └─────┘            
doc                       └─────┘
 66  by simp [has_sum, tendsto_const_nhds]
id            └─────┘  └────────────────┘
src     └────┘└─────┘└┘└────────────────┘└─
typ     └────┘└─────┘└┘└────────────────┘└─
doc     └────┘└─────┘└┘                  └─
txt     └────┘       └┘                  └─
par     └────┘       └┘                  └─
pid                └┘                  
st     └───────────────────────────────────
 67  
src  
typ  
doc  
txt  
par  
pid  
st   
 68  lemma summable_zero : summable (λb, 0 : β → α) := summable_spec has_sum_zero
id                         └──────┘                 └───────────┘ └──────────┘
src                        └──────┘                    └───────────┘ └──────────┘
typ                        └──────┘                 └───────────┘ └──────────┘
doc                        └──────┘                                  └──────────┘
 69  
 70  /-- If a function `f` vanishes outside of a finite set `s`, then it `has_sum` `s.sum f`. -/
 71  lemma has_sum_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : has_sum f (s.sum f) :=
id                                                         └─────┘   └──┘ 
src                                                           └─────┘     └──┘
typ                                                        └─────┘   └──┘ 
doc                                                             └─────┘
 72  tendsto_infi' s $ tendsto.congr'
id   └───────────┘    └────────────┘
src  └───────────┘     └────────────┘
typ  └───────────┘    └────────────┘
 73    (assume t (ht : s ⊆ t), show s.sum f = t.sum f, from sum_subset ht $ assume x _, hf _)
id                              └──┘   └──┘        └────────┘ └┘             └┘
src                                 └──┘     └──┘         └────────┘
typ                             └──┘   └──┘        └────────┘ └┘             └┘
 74    tendsto_const_nhds
id     └────────────────┘
src    └────────────────┘
typ    └────────────────┘
 75  
 76  lemma has_sum_fintype [fintype β] (f : β → α) : has_sum f (finset.univ.sum f) :=
id                          └─────┘               └─────┘   └─────────┘└──┘ 
src                         └─────┘                  └─────┘    └─────────┘└──┘
typ                         └─────┘               └─────┘   └─────────┘└──┘ 
doc                         └─────┘                  └─────┘    └─────────┘
 77  has_sum_sum_of_ne_finset_zero $ λ a h, h.elim (mem_univ _)
id   └───────────────────────────┘        └───┘  └──────┘
src  └───────────────────────────┘           └───┘  └──────┘
typ  └───────────────────────────┘        └───┘  └──────┘
doc  └───────────────────────────┘
 78  
 79  lemma summable_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : summable f :=
id                                                          └──────┘ 
src                                                             └──────┘
typ                                                         └──────┘ 
doc                                                              └──────┘
 80  summable_spec $ has_sum_sum_of_ne_finset_zero hf
id   └───────────┘   └───────────────────────────┘ └┘
src  └───────────┘   └───────────────────────────┘
typ  └───────────┘   └───────────────────────────┘ └┘
doc                  └───────────────────────────┘
 81  
 82  lemma has_sum_single {f : β → α} (b : β) (hf : ∀b' ≠ b, f b' = 0) :
id                                                └┘      └┘ 
src                                                  └┘           
typ                                               └┘      └┘ 
 83    has_sum f (f b) :=
id     └─────┘    
src    └─────┘
typ    └─────┘    
doc    └─────┘
 84  suffices has_sum f (({b} : finset β).sum f),
id            └─────┘        └────┘  └─┘  
src           └─────┘          └────┘   └─┘
typ           └─────┘        └────┘  └─┘  
doc           └─────┘           └────┘
 85    by simpa using this,
id                    └──┘
src       └──────────┘
typ       └──────────┘└──┘
doc       └──────────┘
txt       └──────────┘
par       └──────────┘
pid            └────┘
st       └───────────────┘
 86  has_sum_sum_of_ne_finset_zero $ by simpa [hf]
id   └───────────────────────────┘             └┘
src  └───────────────────────────┘      └─────┘  └─
typ  └───────────────────────────┘      └─────┘└┘└─
doc  └───────────────────────────┘      └─────┘  └─
txt                                     └─────┘  └─
par                                     └─────┘  └─
pid                                            
st                                     └───────────
 87  
src  
typ  
doc  
txt  
par  
pid  
st   
 88  lemma has_sum_ite_eq (b : β) (a : α) : has_sum (λb', if b' = b then a else 0) a :=
id                                        └─────┘   └┘     └┘                 
src                                         └─────┘             
typ                                       └─────┘   └┘     └┘                 
doc                                         └─────┘
 89  begin
st   └─────
 90    convert has_sum_single b _,
id             └────────────┘ 
src    └──────┘└────────────┘ └┘
typ    └──────┘└────────────┘└┘
doc    └──────┘               └┘
txt    └──────┘               └┘
par    └──────┘               └┘
pid                          └┘
st   ───────────────────────────┘└─
 91    { exact (if_pos rfl).symm },
id              └────┘ └─┘
src      └────┘ └────┘└─┘└─────┘
typ      └────┘ └────┘└─┘└─────┘
doc      └────┘          └─────┘
txt      └────┘          └─────┘
par      └────┘          └─────┘
pid                     └───┘└┘
st   ───┘└──────────────────────┘└┘
 92    assume b' hb',
src    └───────────┘
typ    └───────────┘
doc    └───────────┘
txt    └───────────┘
par    └───────────┘
pid    └───────────┘
st   ──────────────┘└─
 93    exact if_neg hb'
id           └────┘ └─┘
src    └────┘└────┘   
typ    └────┘└────┘└─┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                  
st   ──────────────────┘
 94  end
st   └─┘
 95  
 96  lemma has_sum_of_iso {j : γ → β} {i : β → γ}
id                                          
typ                                         
 97    (hf : has_sum f a) (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) : has_sum (f ∘ j) a :=
id           └─────┘                                        └─────┘      
src          └─────┘                                                    └─────┘    
typ          └─────┘                                        └─────┘      
doc          └─────┘                                                      └─────┘
 98  have ∀x y, j x = j y → x = y,
id                     
src                          
typ                    
 99    from assume x y h,
id                   
typ                  
100    have i (j x) = i (j y), by rw [h],
id                             
src                              └──┘ 
typ                        └──┘
doc                               └──┘ 
txt                               └──┘ 
par                               └──┘ 
pid                                 └┘ 
st                               └────┘
101    by rwa [h₁, h₁] at this,
id             └┘  └┘
src       └───┘  └┘  └───────┘
typ       └───┘└┘└┘└┘└───────┘
doc       └───┘  └┘  └───────┘
txt       └───┘  └┘  └───────┘
par       └───┘  └┘  └───────┘
pid          └┘  └┘  └──────┘
st       └──────┘└──┘└──────┘
102  have (λs:finset γ, s.sum (f ∘ j)) = (λs:finset β, s.sum f) ∘ (λs:finset γ, s.image j),
id            └────┘   └──┘            └────┘   └──┘        └────┘   └────┘ 
src           └────┘     └──┘              └────┘     └──┘         └────┘     └────┘
typ           └────┘   └──┘            └────┘   └──┘        └────┘   └────┘ 
doc           └────┘                         └────┘                   └────┘     └────┘
103    from funext $ assume s, (sum_image $ assume x _ y _, this x y).symm,
id          └────┘             └───────┘               └──┘   └──┘
src         └────┘              └───────┘                            └──┘
typ         └────┘             └───────┘               └──┘   └──┘
104  show tendsto (λs:finset γ, s.sum (f ∘ j)) at_top (𝓝 a),
id        └─────┘     └────┘   └──┘       └────┘   
src       └─────┘     └────┘     └──┘         └────┘  
typ       └─────┘     └────┘   └──┘       └────┘   
doc       └─────┘     └────┘                   └────┘  
105     by rw [this]; apply hf.comp (tendsto_finset_image_at_top_at_top h₂)
id             └──┘         └─────┘  └────────────────────────────────┘ └┘
src        └──┘      └────┘└─────┘ └────────────────────────────────┘  └─
typ        └──┘└──┘  └────┘└─────┘ └────────────────────────────────┘└┘└─
doc        └──┘      └────┘                                            └─
txt        └──┘      └────┘                                            └─
par        └──┘      └────┘                                            └─
pid          └┘                                                       
st        └───────┘└───────────────────────────────────────────────────────
106  
src  
typ  
doc  
txt  
par  
pid  
st   
107  lemma has_sum_iff_has_sum_of_iso {j : γ → β} (i : β → γ)
id                                                      
typ                                                     
108    (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) :
id                                     
src                                            
typ                                    
109    has_sum (f ∘ j) a ↔ has_sum f a :=
id     └─────┘        └─────┘  
src    └─────┘           └─────┘
typ    └─────┘        └─────┘  
doc    └─────┘             └─────┘
110  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
111    (assume hfj,
id             └─┘
typ            └─┘
112      have has_sum ((f ∘ j) ∘ i) a, from has_sum_of_iso hfj h₂ h₁,
id            └─────┘                 └────────────┘ └─┘ └┘ └┘
src           └─────┘                     └────────────┘
typ           └─────┘                 └────────────┘ └─┘ └┘ └┘
doc           └─────┘
113      by simp [(∘), h₂] at this; assumption)
id                    └┘
src         └────┘└──┘  └───────┘  └────────┘
typ         └────┘└──┘└┘└───────┘  └────────┘
doc         └────┘ └──┘  └───────┘  └────────┘
txt         └────┘ └──┘  └───────┘  └────────┘
par         └────┘ └──┘  └───────┘  └────────┘
pid              └──┘  └─────┘
st         └─────────────────────────────────┘
114    (assume hf, has_sum_of_iso hf h₁ h₂)
id             └┘  └────────────┘ └┘ └┘ └┘
src                └────────────┘
typ            └┘  └────────────┘ └┘ └┘ └┘
115  
116  lemma has_sum_hom (g : α → γ) [add_comm_monoid γ] [topological_space γ]
id                                └─────────────┘    └───────────────┘ 
src                                 └─────────────┘     └───────────────┘
typ                               └─────────────┘    └───────────────┘ 
doc                                                     └───────────────┘
117    [is_add_monoid_hom g] (h₃ : continuous g) (hf : has_sum f a) :
id      └───────────────┘         └────────┘         └─────┘  
src     └───────────────┘          └────────┘          └─────┘
typ     └───────────────┘         └────────┘         └─────┘  
doc     └───────────────┘          └────────┘          └─────┘
118    has_sum (g ∘ f) (g a) :=
id     └─────┘        
src    └─────┘    
typ    └─────┘        
doc    └─────┘
119  have (λs:finset β, s.sum (g ∘ f)) = g ∘ (λs:finset β, s.sum f),
id            └────┘   └──┘              └────┘   └──┘ 
src           └────┘     └──┘                 └────┘     └──┘
typ           └────┘   └──┘              └────┘   └──┘ 
doc           └────┘                             └────┘
120    from funext $ assume s, s.sum_hom g,
id          └────┘            └──────┘ 
src         └────┘              └──────┘
typ         └────┘            └──────┘ 
121  show tendsto (λs:finset β, s.sum (g ∘ f)) at_top (𝓝 (g a)),
id        └─────┘     └────┘   └──┘       └────┘     
src       └─────┘     └────┘     └──┘         └────┘  
typ       └─────┘     └────┘   └──┘       └────┘     
doc       └─────┘     └────┘                   └────┘  
122    by rw [this]; exact tendsto.comp (continuous_iff_continuous_at.mp h₃ a) hf
id            └──┘         └──────────┘  └─────────────────────────────┘ └┘   └┘
src       └──┘      └────┘└──────────┘ └─────────────────────────────┘   └┘  
typ       └──┘└──┘  └────┘└──────────┘ └─────────────────────────────┘└┘└┘└┘
doc       └──┘      └────┘                                               └┘  
txt       └──┘      └────┘                                               └┘  
par       └──┘      └────┘                                               └┘  
pid         └┘                                                          └┘  
st       └───────┘└──────────────────────────────────────────────────────────────
123  
src  
typ  
doc  
txt  
par  
pid  
st   
124  /-- If `f : ℕ → α` has sum `a`, then the partial sums `∑_{i=0}^{n-1} f i` converge to `a`. -/
125  lemma tendsto_sum_nat_of_has_sum {f : ℕ → α} (h : has_sum f a) :
id                                                   └─────┘  
src                                                   └─────┘
typ                                                  └─────┘  
doc                                                    └─────┘
126    tendsto (λn:ℕ, (range n).sum f) at_top (𝓝 a) :=
id     └─────┘        └───┘  └─┘    └────┘   
src    └─────┘        └───┘   └─┘     └────┘  
typ    └─────┘        └───┘  └─┘    └────┘   
doc    └─────┘         └───┘           └────┘  
127  @tendsto.comp _ _ _ finset.range (λ s : finset ℕ, s.sum f) _ _ _ h tendsto_finset_range
id    └──────────┘       └──────────┘        └────┘   └──┘          └──────────────────┘
src   └──────────┘       └──────────┘        └────┘    └──┘            └──────────────────┘
typ   └──────────┘       └──────────┘        └────┘   └──┘          └──────────────────┘
doc                      └──────────┘        └────┘
128  
129  variable [topological_add_monoid α]
id             └────────────────────┘
src            └────────────────────┘
typ            └────────────────────┘
doc            └────────────────────┘
130  
131  lemma has_sum_add (hf : has_sum f a) (hg : has_sum g b) : has_sum (λb, f b + g b) (a + b) :=
id                           └─────┘          └─────┘      └─────┘              
src                          └─────┘            └─────┘        └─────┘                   
typ                          └─────┘          └─────┘      └─────┘              
doc                          └─────┘            └─────┘        └─────┘
132  by simp [has_sum, sum_add_distrib]; exact hf.add hg
id            └─────┘  └─────────────┘         └────┘ └┘
src     └────┘└─────┘└┘└─────────────┘  └────┘└────┘  
typ     └────┘└─────┘└┘└─────────────┘  └────┘└────┘└┘
doc     └────┘└─────┘└┘                 └────┘        
txt     └────┘       └┘                 └────┘        
par     └────┘       └┘                 └────┘        
pid                └┘                              
st     └─────────────────────────────────────────────────
133  
src  
typ  
doc  
txt  
par  
pid  
st   
134  lemma summable_add (hf : summable f) (hg : summable g) : summable (λb, f b + g b) :=
id                            └──────┘         └──────┘     └──────┘         
src                           └──────┘          └──────┘      └──────┘          
typ                           └──────┘         └──────┘     └──────┘         
doc                           └──────┘          └──────┘      └──────┘
135  summable_spec $ has_sum_add (has_sum_tsum hf)(has_sum_tsum hg)
id   └───────────┘   └─────────┘  └──────────┘ └┘  └──────────┘ └┘
src  └───────────┘   └─────────┘  └──────────┘     └──────────┘
typ  └───────────┘   └─────────┘  └──────────┘ └┘  └──────────┘ └┘
136  
137  lemma has_sum_sum {f : γ → β → α} {a : γ → α} {s : finset γ} :
id                                                 └────┘ 
src                                                     └────┘
typ                                                └────┘ 
doc                                                     └────┘
138    (∀i∈s, has_sum (f i) (a i)) → has_sum (λb, s.sum $ λi, f i b) (s.sum a) :=
id          └─────┘            └─────┘     └──┘           └──┘ 
src           └─────┘                └─────┘       └──┘                └──┘
typ         └─────┘            └─────┘     └──┘           └──┘ 
doc           └─────┘                └─────┘
139  finset.induction_on s (by simp [has_sum_zero]) (by simp [has_sum_add] {contextual := tt})
id   └─────────────────┘            └──────────┘             └─────────┘                 └┘
src  └─────────────────┘       └────┘└──────────┘      └────┘└─────────┘└┘ └────────────┘└┘
typ  └─────────────────┘      └────┘└──────────┘      └────┘└─────────┘└┘ └────────────┘└┘
doc  └─────────────────┘       └────┘└──────────┘      └────┘           └┘ └────────────┘  
txt                            └────┘                  └────┘           └┘ └────────────┘  
par                            └────┘                  └────┘           └┘ └────────────┘  
pid                                                                  └────────────┘  
st                            └──────────────────┘     └────────────────────────────────────┘
140  
141  lemma summable_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summable (f i)) :
id                                        └────┘             └──────┘   
src                                          └────┘                └──────┘
typ                                       └────┘             └──────┘   
doc                                          └────┘                └──────┘
142    summable (λb, s.sum $ λi, f i b) :=
id     └──────┘     └──┘        
src    └──────┘       └──┘
typ    └──────┘     └──┘        
doc    └──────┘
143  summable_spec $ has_sum_sum $ assume i hi, has_sum_tsum $ hf i hi
id   └───────────┘   └─────────┘           └┘  └──────────┘   └┘  └┘
src  └───────────┘   └─────────┘                └──────────┘
typ  └───────────┘   └─────────┘           └┘  └──────────┘   └┘  └┘
144  
145  lemma has_sum_sigma [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
id                        └───────────┘                                                  
src                       └───────────┘                              
typ                       └───────────┘                                                  
doc                       └───────────┘
146    (hf : ∀b, has_sum (λc, f ⟨b, c⟩) (g b)) (ha : has_sum f a) : has_sum g a :=
id              └─────┘                       └─────┘      └─────┘  
src              └─────┘                             └─────┘        └─────┘
typ             └─────┘                       └─────┘      └─────┘  
doc              └─────┘                             └─────┘        └─────┘
147  assume s' hs',
148  let
149    ⟨s, hs, hss', hsc⟩ := nhds_is_closed hs',
id                           └────────────┘
src                          └────────────┘
typ                          └────────────┘
150    ⟨u, hu⟩ := mem_at_top_sets.mp $ ha hs,
151    fsts := u.image sigma.fst,
id                     └───────┘
src                    └───────┘
typ                    └───────┘
152    snds := λb, u.bind (λp, (if h : p.1 = b then {cast (congr_arg γ h) p.2} else ∅ : finset (γ b)))
id                                                         └───────┘                    └────┘
src                                                        └───────┘                    └────┘
typ                                                        └───────┘                    └────┘
doc                                                                                     └────┘
153  in
154  have u_subset : u ⊆ fsts.sigma snds,
155    from subset_iff.mpr $ assume ⟨b, c⟩ hu,
156    have hb : b ∈ fsts, from finset.mem_image.mpr ⟨_, hu, rfl⟩,
id                                                           └─┘
src                                                          └─┘
typ                                                          └─┘
157    have hc : c ∈ snds b, from mem_bind.mpr ⟨_, hu, by simp; refl⟩,
src                                                       └──┘  └──┘
typ                                                       └──┘  └──┘
doc                                                       └──┘  └──┘
txt                                                       └──┘  └──┘
par                                                       └──┘  └──┘
158    by simp [mem_sigma, hb, hc] ,
src       └────┘         └┘  └┘  └┘
typ       └────┘         └┘  └┘  └┘
doc       └────┘         └┘  └┘  └┘
txt       └────┘         └┘  └┘  └┘
par       └────┘         └┘  └┘  └┘
pid                    └┘  └┘  
159  mem_at_top_sets.mpr $ exists.intro fsts $ assume bs (hbs : fsts ⊆ bs),
id                         └──────────┘
src                        └──────────┘
typ                        └──────────┘
160    have h : ∀cs : Π b ∈ bs, finset (γ b),
id                              └────┘
src                             └────┘
typ                             └────┘
doc                             └────┘
161        ((⋂b (hb : b ∈ bs), (λp:Πb, finset (γ b), p b) ⁻¹' {cs' | cs b hb ⊆ cs' }) ∩
id                                     └────┘
src                                    └────┘
typ                                    └────┘
doc                                    └────┘
162        (λp, bs.sum (λb, (p b).sum (λc, f ⟨b, c⟩))) ⁻¹' s).nonempty,
163      from assume cs,
164      let cs' := λb, (if h : b ∈ bs then cs b h else ∅) ∪ snds b in
165      have sum_eq : bs.sum (λb, (cs' b).sum (λc, f ⟨b, c⟩)) = (bs.sigma cs').sum f,
166        from sum_sigma.symm,
167      have (bs.sigma cs').sum f ∈ s,
168        from hu _ $ finset.subset.trans u_subset $ sigma_mono hbs $
id                     └─────────────────┘            └────────┘
src                    └─────────────────┘            └────────┘
typ                    └─────────────────┘            └────────┘
169          assume b, @finset.subset_union_right (γ b) _ _ _,
id                      └───────────────────────┘
src                     └───────────────────────┘
typ                     └───────────────────────┘
170      exists.intro cs' $
id       └──────────┘
src      └──────────┘
typ      └──────────┘
171      by simp [sum_eq, this]; { intros b hb, simp [cs', hb, finset.subset_union_right] },
src         └────┘      └┘        └─────────┘  └────┘   └┘  └┘                         └┘
typ         └────┘      └┘        └─────────┘  └────┘   └┘  └┘                         └┘
doc         └────┘      └┘        └─────────┘  └────┘   └┘  └┘                         └┘
txt         └────┘      └┘        └─────────┘  └────┘   └┘  └┘                         └┘
par         └────┘      └┘        └─────────┘  └────┘   └┘  └┘                         └┘
pid                   └┘              └───┘         └┘  └┘                         
172    have tendsto (λp:(Πb:β, finset (γ b)), bs.sum (λb, (p b).sum (λc, f ⟨b, c⟩)))
id                             └────┘
src                            └────┘
typ                            └────┘
doc                            └────┘
173        (⨅b (h : b ∈ bs), at_top.comap (λp, p b)) (𝓝 (bs.sum g)),
174      from tendsto_finset_sum bs $
id            └────────────────┘
src           └────────────────┘
typ           └────────────────┘
175        assume c hc, tendsto_infi' c $ tendsto_infi' hc $ by apply tendsto.comp (hf c) tendsto_comap,
id                      └───────────┘     └───────────┘
src                     └───────────┘     └───────────┘         └────┘                └┘
typ                     └───────────┘     └───────────┘         └────┘                └┘
doc                                                             └────┘                └┘
txt                                                             └────┘                └┘
par                                                             └────┘                └┘
pid                                                                                  └┘
176    have bs.sum g ∈ s,
177      from mem_of_closed_of_tendsto' this hsc $ forall_sets_nonempty_iff_ne_bot.mp $
id            └───────────────────────┘
src           └───────────────────────┘
typ           └───────────────────────┘
178        by simp [mem_inf_sets, exists_imp_distrib, and_imp, forall_and_distrib,
id                                         └───────┘  └─────┘  └────────────────┘
src           └────┘            └┘         └───────┘└┘└─────┘└┘└────────────────┘└─
typ           └────┘            └┘         └───────┘└┘└─────┘└┘└────────────────┘└─
doc           └────┘            └┘                  └┘       └┘                  └─
txt           └────┘            └┘                  └┘       └┘                  └─
par           └────┘            └┘                  └┘       └┘                  └─
pid                           └┘                  └┘       └┘                  └─
st                                         └───────────────────────────────────────
179                 filter.mem_infi_sets_finset, mem_comap_sets, skolem, mem_at_top_sets,
id                  └─────────────────────────┘  └────────────┘  └────┘  └─────────────┘
src  ──────────────┘└─────────────────────────┘└┘└────────────┘└┘└────┘└┘└─────────────┘└─
typ  ──────────────┘└─────────────────────────┘└┘└────────────┘└┘└────┘└┘└─────────────┘└─
doc  ──────────────┘                           └┘              └┘      └┘               └─
txt  ──────────────┘                           └┘              └┘      └┘               └─
par  ──────────────┘                           └┘              └┘      └┘               └─
pid  ──────────────┘                           └┘              └┘      └┘               └─
st   ─────────────────────────────────────────────────────────────────────────────────────
180                 and_comm];
id                  └──────┘
src  ──────────────┘└──────┘
typ  ──────────────┘└──────┘
doc  ──────────────┘        
txt  ──────────────┘        
par  ──────────────┘        
pid  ──────────────┘        
st   ──────────────────────────
181        from
src        └────
typ        └────
doc        └────
txt        └────
par        └────
pid        └────
st   ───────────
182          assume s₁ s₂ s₃ hs₁ hs₃ p hs₂ p' hp cs hp',
src  ───────┘      └─────────────────────────────────────
typ  ───────┘      └─────────────────────────────────────
doc  ───────┘      └─────────────────────────────────────
txt  ───────┘      └─────────────────────────────────────
par  ───────┘      └─────────────────────────────────────
pid  ───────┘      └─────────────────────────────────────
st   ────────────────────────────────────────────────────
183          have (⋂b (h : b ∈ bs), (λp:(Πb, finset (γ b)), p b) ⁻¹' {cs' | cs b h ⊆ cs' }) ≤ (⨅b∈bs, p b),
id                                        └────┘             └─┘                          └┘
src  ───────┘     └─────┘     └┘   └────┘   └──┘  └┘└─┘└────┘       └──┘ └┘    └──
typ  ───────┘     └─────┘     └┘   └────┘  └──┘  └┘└─┘└────┘       └──┘ └┘└┘  └──
doc  ───────┘     └─────┘      └┘   └────┘   └──┘  └┘└─┘ └────┘        └──┘  └┘    └──
txt  ───────┘      └─────┘       └┘            └──┘  └┘    └────┘        └──┘   └┘     └──
par  ───────┘      └─────┘       └┘            └──┘  └┘    └────┘        └──┘   └┘     └──
pid  ───────┘      └─────┘       └┘            └──┘  └┘    └────┘        └──┘   └┘     └──
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────
184            from infi_le_infi $ assume b, infi_le_infi $ assume hb,
id                                           └──────────┘
src  ──────────────┘                   └──┘└──────────┘       └────
typ  ──────────────┘                   └──┘└──────────┘       └────
doc  ──────────────┘                   └──┘                   └────
txt  ──────────────┘                   └──┘                   └────
par  ──────────────┘                   └──┘                   └────
pid  ──────────────┘                   └──┘                   └────
st   ──────────────────────────────────────────────────────────────────
185              le_trans (set.preimage_mono $ hp' b hb) (hp b hb),
id               └──────┘  └───────────────┘
src  ───────────┘└──────┘ └───────────────┘       └┘      └──
typ  ───────────┘└──────┘ └───────────────┘       └┘      └──
doc  ───────────┘                                 └┘      └──
txt  ───────────┘                                 └┘      └──
par  ───────────┘                                 └┘      └──
pid  ───────────┘                                 └┘      └──
st   ───────────────────────────────────────────────────────────────
186          (h _).mono (set.subset.trans (set.inter_subset_inter (le_trans this hs₂) hs₃) hs₁),
id                      └──────────────┘  └────────────────────┘
src  ───────┘  └───────┘ └──────────────┘ └────────────────────┘                └┘   └┘   
typ  ───────┘ └───────┘ └──────────────┘ └────────────────────┘                └┘   └┘   
doc  ───────┘  └───────┘                                                        └┘   └┘   
txt  ───────┘  └───────┘                                                        └┘   └┘   
par  ───────┘  └───────┘                                                        └┘   └┘   
pid  ───────┘  └───────┘                                                        └┘   └┘   
st   ─────────────────────────────────────────────────────────────────────────────────────────┘
187    hss' this
id          └──┘
typ         └──┘
188  
189  lemma summable_sigma [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
id                         └───────────┘                                
src                        └───────────┘                             
typ                        └───────────┘                                
doc                        └───────────┘
190    (hf : ∀b, summable (λc, f ⟨b, c⟩)) (ha : summable f) : summable (λb, ∑c, f ⟨b, c⟩) :=
id              └──────┘                   └──────┘     └──────┘          
src              └──────┘                       └──────┘      └──────┘       
typ             └──────┘                   └──────┘     └──────┘          
doc              └──────┘                       └──────┘      └──────┘       
191  summable_spec $ has_sum_sigma (assume b, has_sum_tsum $ hf b) (has_sum_tsum ha)
id   └───────────┘   └───────────┘           └──────────┘   └┘    └──────────┘ └┘
src  └───────────┘   └───────────┘            └──────────┘          └──────────┘
typ  └───────────┘   └───────────┘           └──────────┘   └┘    └──────────┘ └┘
192  
193  end has_sum
194  
195  section has_sum_iff_has_sum_of_iso_ne_zero
196  variables [add_comm_monoid α] [topological_space α]
id              └─────────────┘     └───────────────┘
src             └─────────────┘     └───────────────┘
typ             └─────────────┘     └───────────────┘
doc                                 └───────────────┘
197  variables {f : β → α} {g : γ → α} {a : α}
198  
199  lemma has_sum_of_has_sum
200    (h_eq : ∀u:finset γ, ∃v:finset β, ∀v', v ⊆ v' → ∃u', u ⊆ u' ∧ u'.sum g = v'.sum f)
id                └────┘     └────┘   └┘    └┘   └┘   └┘  └┘└──┘   └┘└──┘ 
src               └────┘      └────┘                            └──┘      └──┘
typ               └────┘     └────┘   └┘    └┘   └┘   └┘  └┘└──┘   └┘└──┘ 
doc               └────┘       └────┘
201    (hf : has_sum g a) : has_sum f a :=
id           └─────┘      └─────┘  
src          └─────┘        └─────┘
typ          └─────┘      └─────┘  
doc          └─────┘        └─────┘
202  suffices at_top.map (λs:finset β, s.sum f) ≤ at_top.map (λs:finset γ, s.sum g),
id            └────┘└──┘     └────┘   └──┘    └────┘└──┘     └────┘   └──┘ 
src           └────┘└──┘     └────┘     └──┘     └────┘└──┘     └────┘     └──┘
typ           └────┘└──┘     └────┘   └──┘    └────┘└──┘     └────┘   └──┘ 
doc           └────┘└──┘     └────┘               └────┘└──┘     └────┘
203    from le_trans this hf,
id          └──────┘ └──┘ └┘
src         └──────┘
typ         └──────┘ └──┘ └┘
204  by rw [map_at_top_eq, map_at_top_eq];
id          └───────────┘  └───────────┘
src     └──┘└───────────┘└┘└───────────┘
typ     └──┘└───────────┘└┘└───────────┘
doc     └──┘             └┘             
txt     └──┘             └┘             
par     └──┘             └┘             
pid       └┘             └┘             
st     └────────────────┘└─────────────┘└─
205  from (le_infi $ assume b, let ⟨v, hv⟩ := h_eq b in infi_le_of_le v $
id         └─────┘                           └──┘      └───────────┘
src  └───┘ └─────┘       └──┘     └┘  └───┘     └──┘└───────────┘  
typ  └───┘ └─────┘       └──┘    └┘  └───┘└──┘ └──┘└───────────┘  
doc  └───┘               └──┘     └┘  └───┘     └──┘               
txt  └───┘               └──┘     └┘  └───┘     └──┘               
par  └───┘               └──┘     └┘  └───┘     └──┘               
pid  └───┘               └──┘     └┘  └───┘     └──┘               
st   ─────────────────────────────────────────────────────────────────────
206    by simp [set.image_subset_iff]; exact hv)
id              └──────────────────┘         └┘
src  ─┘  └────┘└──────────────────┘└┘└────┘  └─
typ  ─┘  └────┘└──────────────────┘└──────┘└┘└─
doc  ─┘  └────┘└──────────────────┘└┘└────┘  └─
txt  ─┘  └────┘                    └┘└────┘  └─
par  ─┘  └────┘                    └──────┘  └─
pid  ─┘  └─────┘                    └───────┘  
st   ───┘└────────────────────────────────────┘└─
207  
src  
typ  
doc  
txt  
par  
pid  
st   
208  lemma has_sum_iff_has_sum
209    (h₁ : ∀u:finset γ, ∃v:finset β, ∀v', v ⊆ v' → ∃u', u ⊆ u' ∧ u'.sum g = v'.sum f)
id              └────┘     └────┘   └┘    └┘   └┘   └┘  └┘└──┘   └┘└──┘ 
src             └────┘      └────┘                            └──┘      └──┘
typ             └────┘     └────┘   └┘    └┘   └┘   └┘  └┘└──┘   └┘└──┘ 
doc             └────┘       └────┘
210    (h₂ : ∀v:finset β, ∃u:finset γ, ∀u', u ⊆ u' → ∃v', v ⊆ v' ∧ v'.sum f = u'.sum g) :
id              └────┘     └────┘   └┘    └┘   └┘   └┘  └┘└──┘   └┘└──┘ 
src             └────┘      └────┘                            └──┘      └──┘
typ             └────┘     └────┘   └┘    └┘   └┘   └┘  └┘└──┘   └┘└──┘ 
doc             └────┘       └────┘
211    has_sum f a ↔ has_sum g a :=
id     └─────┘    └─────┘  
src    └─────┘      └─────┘
typ    └─────┘    └─────┘  
doc    └─────┘       └─────┘
212  ⟨has_sum_of_has_sum h₂, has_sum_of_has_sum h₁⟩
id    └────────────────┘ └┘  └────────────────┘ └┘
src   └────────────────┘     └────────────────┘
typ   └────────────────┘ └┘  └────────────────┘ └┘
213  
214  variables
215    (i : Π⦃c⦄, g c ≠ 0 → β) (hi : ∀⦃c⦄ (h : g c ≠ 0), f (i h) ≠ 0)
id                                                        
src                                                            
typ                                                       
216    (j : Π⦃b⦄, f b ≠ 0 → γ) (hj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) ≠ 0)
id                                                        
src                                                            
typ                                                       
217    (hji : ∀⦃c⦄ (h : g c ≠ 0), j (hi h) = c)
id                                      
src                                       
typ                                     
218    (hij : ∀⦃b⦄ (h : f b ≠ 0), i (hj h) = b)
id                                      
src                                       
typ                                     
219    (hgj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) = f b)
id                                       
src                                      
typ                                      
220  include hi hj hji hij hgj
221  
222  lemma has_sum_of_has_sum_ne_zero : has_sum g a → has_sum f a :=
id                                      └─────┘     └─────┘  
src                                     └─────┘       └─────┘
typ                                     └─────┘     └─────┘  
doc                                     └─────┘       └─────┘
223  have j_inj : ∀x y (hx : f x ≠ 0) (hy : f y ≠ 0), (j hx = j hy ↔ x = y),
id                                              └┘   └┘    
src                                                                
typ                                             └┘   └┘    
224    from assume x y hx hy,
id                   └┘ └┘
typ                  └┘ └┘
225    ⟨assume h,
id             
typ            
226      have i (hj hx) = i (hj hy), by simp [h],
id              └┘ └┘     └┘ └┘            
src                                    └────┘ 
typ             └┘ └┘     └┘ └┘      └────┘
doc                                     └────┘ 
txt                                     └────┘ 
par                                     └────┘ 
pid                                          
st                                     └───────┘
227      by rwa [hij, hij] at this; assumption,
id               └─┘  └─┘
src         └───┘   └┘   └───────┘  └────────┘
typ         └───┘└─┘└┘└─┘└───────┘  └────────┘
doc         └───┘   └┘   └───────┘  └────────┘
txt         └───┘   └┘   └───────┘  └────────┘
par         └───┘   └┘   └───────┘  └────────┘
pid            └┘   └┘   └──────┘
st         └───────┘└───┘└──────────────────┘
228    by simp {contextual := tt}⟩,
id                            └┘
src       └───┘ └────────────┘└┘
typ       └───┘ └────────────┘└┘
doc       └───┘ └────────────┘  
txt       └───┘ └────────────┘  
par       └───┘ └────────────┘  
pid            └────────────┘  
st       └──────────────────────┘
229  let ii : finset γ → finset β := λu, u.bind $ λc, if h : g c = 0 then ∅ else {i h} in
id            └────┘   └────┘        └───┘      └┘                      
src           └────┘     └────┘           └───┘       └┘                       
typ           └────┘   └────┘        └───┘      └┘                      
doc           └────┘     └────┘           └───┘
230  let jj : finset β → finset γ := λv, v.bind $ λb, if h : f b = 0 then ∅ else {j h} in
id            └────┘   └────┘        └───┘      └┘                      
src           └────┘     └────┘           └───┘       └┘                       
typ           └────┘   └────┘        └───┘      └┘                      
doc           └────┘     └────┘           └───┘
231  has_sum_of_has_sum $ assume u, exists.intro (ii u) $
id   └────────────────┘            └──────────┘  └┘ 
src  └────────────────┘             └──────────┘
typ  └────────────────┘            └──────────┘  └┘ 
232    assume v hv, exists.intro (u ∪ jj v) $ and.intro (subset_union_left _ _) $
id             └┘  └──────────┘    └┘     └───────┘  └───────────────┘
src                 └──────────┘             └───────┘  └───────────────┘
typ            └┘  └──────────┘    └┘     └───────┘  └───────────────┘
233    have ∀c:γ, c ∈ u ∪ jj v → c ∉ jj v → g c = 0,
id                   └┘      └┘      
src                                          
typ                  └┘      └┘      
234      from assume c hc hnc, classical.by_contradiction $ assume h : g c ≠ 0,
id                    └┘ └─┘  └────────────────────────┘                
src                            └────────────────────────┘                  
typ                   └┘ └─┘  └────────────────────────┘                
235      have c ∈ u,
id              
src             
typ             
236        from (finset.mem_union.1 hc).resolve_right hnc,
id               └──────────────┘  └┘ └───────────┘  └─┘
src              └──────────────┘     └───────────┘
typ              └──────────────┘  └┘ └───────────┘  └─┘
237      have i h ∈ v,
id               
src               
typ              
238        from hv $ by simp [mem_bind]; existsi c; simp [h, this],
id              └┘            └──────┘                     └──┘
src                     └────┘└──────┘  └──────┘   └────┘ └┘    
typ             └┘      └────┘└──────┘  └──────┘  └────┘└┘└──┘
doc                     └────┘          └──────┘   └────┘ └┘    
txt                     └────┘          └──────┘   └────┘ └┘    
par                     └────┘          └──────┘   └────┘ └┘    
pid                                                  └┘    
st                     └─────────────────────────────────────────┘
239      have j (hi h) ∈ jj v,
id              └┘    └┘ 
src                    
typ             └┘    └┘ 
240        by simp [mem_bind]; existsi i h; simp [h, hi, this],
id                  └──────┘                      └┘  └──┘
src           └────┘└──────┘  └──────┘    └────┘ └┘  └┘    
typ           └────┘└──────┘  └──────┘  └────┘└┘└┘└┘└──┘
doc           └────┘          └──────┘    └────┘ └┘  └┘    
txt           └────┘          └──────┘    └────┘ └┘  └┘    
par           └────┘          └──────┘    └────┘ └┘  └┘    
pid                                         └┘  └┘    
st           └───────────────────────────────────────────────┘
241      by rw [hji h] at this; exact hnc this,
id              └─┘                  └─┘ └──┘
src         └──┘    └───────┘  └────┘   
typ         └──┘└─┘└───────┘  └────┘└─┘└──┘
doc         └──┘    └───────┘  └────┘   
txt         └──┘    └───────┘  └────┘   
par         └──┘    └───────┘  └────┘   
pid           └┘    └──────┘          
st         └────────┘└──────────────────────┘
242    calc (u ∪ jj v).sum g = (jj v).sum g : (sum_subset (subset_union_right _ _) this).symm
id             └┘  └─┘      └┘  └─┘      └────────┘  └────────────────┘      └──┘ └──┘
src                  └─┘            └─┘       └────────┘  └────────────────┘           └──┘
typ            └┘  └─┘      └┘  └─┘      └────────┘  └────────────────┘      └──┘ └──┘
243      ... = v.sum _ : sum_bind $ by intros x _ y _ _; by_cases f x = 0; by_cases f y = 0; simp [*]; cc
id             └──┘     └──────┘                                                 
src             └──┘     └──────┘      └──────────────┘  └───────┘  └┘  └───────┘   └┘  └──────┘  └──
typ            └──┘     └──────┘      └──────────────┘  └───────┘└┘  └───────┘ └┘  └──────┘  └──
doc                                    └──────────────┘  └───────┘   └┘  └───────┘   └┘  └──────┘  └──
txt                                    └──────────────┘  └───────┘   └┘  └───────┘   └┘  └──────┘  └──
par                                    └──────────────┘  └───────┘   └┘  └───────┘   └┘  └──────┘  └──
pid                                          └────────┘                                └─┘    
st                                    └───────────────────────────────────────────────────────────────────
244      ... = v.sum f : sum_congr rfl $ by intros x hx; by_cases f x = 0; simp [*]
id             └──┘    └───────┘ └─┘                             
src  ───┘       └──┘     └───────┘ └─┘      └─────────┘  └───────┘   └┘  └────────
typ  ───┘      └──┘    └───────┘ └─┘      └─────────┘  └───────┘ └┘  └────────
doc  ───┘                                   └─────────┘  └───────┘   └┘  └────────
txt  ───┘                                   └─────────┘  └───────┘   └┘  └────────
par  ───┘                                   └─────────┘  └───────┘   └┘  └────────
pid  ───┘                                         └───┘                   └─┘
st   ───┘                                  └────────────────────────────────────────
245  
src  
typ  
doc  
txt  
par  
pid  
st   
246  lemma has_sum_iff_has_sum_of_ne_zero : has_sum f a ↔ has_sum g a :=
id                                          └─────┘    └─────┘  
src                                         └─────┘      └─────┘
typ                                         └─────┘    └─────┘  
doc                                         └─────┘       └─────┘
247  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
248    (has_sum_of_has_sum_ne_zero j hj i hi hij hji $ assume b hb, by rw [←hgj (hi _), hji])
id      └────────────────────────┘  └┘  └┘ └─┘ └─┘           └┘          └─┘  └┘     └─┘
src     └────────────────────────┘                                     └───┘      └───┘   
typ     └────────────────────────┘  └┘  └┘ └─┘ └─┘           └┘     └───┘└─┘ └┘└───┘└─┘
doc                                                                    └───┘      └───┘   
txt                                                                    └───┘      └───┘   
par                                                                    └───┘      └───┘   
pid                                                                      └─┘      └───┘   
st                                                                    └──────────────┘└───┘
249    (has_sum_of_has_sum_ne_zero i hi j hj hji hij hgj)
id      └────────────────────────┘  └┘  └┘ └─┘ └─┘ └─┘
src     └────────────────────────┘
typ     └────────────────────────┘  └┘  └┘ └─┘ └─┘ └─┘
250  
251  lemma summable_iff_summable_ne_zero : summable g ↔ summable f :=
id                                         └──────┘   └──────┘ 
src                                        └──────┘    └──────┘
typ                                        └──────┘   └──────┘ 
doc                                        └──────┘     └──────┘
252  exists_congr $
id   └──────────┘
src  └──────────┘
typ  └──────────┘
253    assume a, has_sum_iff_has_sum_of_ne_zero j hj i hi hij hji $
id              └────────────────────────────┘  └┘  └┘ └─┘ └─┘
src              └────────────────────────────┘
typ             └────────────────────────────┘  └┘  └┘ └─┘ └─┘
254      assume b hb, by rw [←hgj (hi _), hji]
id               └┘          └─┘  └┘     └─┘
src                      └───┘      └───┘   └─
typ              └┘     └───┘└─┘ └┘└───┘└─┘└─
doc                      └───┘      └───┘   └─
txt                      └───┘      └───┘   └─
par                      └───┘      └───┘   └─
pid                        └─┘      └───┘   
st                      └──────────────┘└───┘
255  
src  
typ  
doc  
txt  
par  
pid  
st   
256  end has_sum_iff_has_sum_of_iso_ne_zero
257  
258  section has_sum_iff_has_sum_of_bij_ne_zero
259  variables [add_comm_monoid α] [topological_space α]
id              └─────────────┘     └───────────────┘
src             └─────────────┘     └───────────────┘
typ             └─────────────┘     └───────────────┘
doc                                 └───────────────┘
260  variables {f : β → α} {g : γ → α} {a : α}
261    (i : Π⦃c⦄, g c ≠ 0 → β)
id                  
src                   
typ                 
262    (h₁ : ∀⦃c₁ c₂⦄ (h₁ : g c₁ ≠ 0) (h₂ : g c₂ ≠ 0), i h₁ = i h₂ → c₁ = c₂)
id             └┘ └┘          └┘             └┘        └┘    └┘   └┘  └┘
src                                                                  
typ            └┘ └┘          └┘             └┘        └┘    └┘   └┘  └┘
263    (h₂ : ∀⦃b⦄, f b ≠ 0 → ∃c (h : g c ≠ 0), i h = b)
id                                         
src                                            
typ                                        
264    (h₃ : ∀⦃c⦄ (h : g c ≠ 0), f (i h) = g c)
id                                      
src                                     
typ                                     
265  include i h₁ h₂ h₃
266  
267  lemma has_sum_iff_has_sum_of_ne_zero_bij : has_sum f a ↔ has_sum g a :=
id                                              └─────┘    └─────┘  
src                                             └─────┘      └─────┘
typ                                             └─────┘    └─────┘  
doc                                             └─────┘       └─────┘
268  have hi : ∀⦃c⦄ (h : g c ≠ 0), f (i h) ≠ 0,
id                                  
src                                       
typ                                 
269    from assume c h, by simp [h₃, h],
id                             └┘  
src                        └────┘  └┘ 
typ                      └────┘└┘└┘
doc                        └────┘  └┘ 
txt                        └────┘  └┘ 
par                        └────┘  └┘ 
pid                              └┘ 
st                        └───────────┘
270  let j : Π⦃b⦄, f b ≠ 0 → γ := λb h, some $ h₂ h in
id                              └──┘   └┘ 
src                                    └──┘
typ                             └──┘   └┘ 
271  have hj : ∀⦃b⦄ (h : f b ≠ 0), ∃(h : g (j h) ≠ 0), i h = b,
id                                              
src                                                    
typ                                             
272    from assume b h, some_spec $ h₂ h,
id                    └───────┘   └┘ 
src                     └───────┘
typ                   └───────┘   └┘ 
273  have hj₁ : ∀⦃b⦄ (h : f b ≠ 0), g (j h) ≠ 0,
id                                   
src                                        
typ                                  
274    from assume b h, let ⟨h₁, _⟩ := hj h in h₁,
id                    └─┘  └┘        └┘ 
typ                   └─┘  └┘        └┘ 
275  have hj₂ : ∀⦃b⦄ (h : f b ≠ 0), i (hj₁ h) = b,
id                                └─┘    
src                                          
typ                               └─┘    
276    from assume b h, let ⟨h₁, h₂⟩ := hj h in h₂,
id                    └─┘      └┘     └┘ 
typ                   └─┘      └┘     └┘ 
277  has_sum_iff_has_sum_of_ne_zero i hi j hj₁
id   └────────────────────────────┘  └┘  └─┘
src  └────────────────────────────┘
typ  └────────────────────────────┘  └┘  └─┘
278    (assume c h, h₁ (hj₁ _) h $ hj₂ _) hj₂ (assume b h, by rw [←h₃ (hj₁ _), hj₂])
id                └┘  └─┘       └─┘    └─┘                    └┘  └─┘     └─┘
src                                                           └───┘      └───┘   
typ               └┘  └─┘       └─┘    └─┘               └───┘└┘ └─┘└───┘└─┘
doc                                                           └───┘      └───┘   
txt                                                           └───┘      └───┘   
par                                                           └───┘      └───┘   
pid                                                             └─┘      └───┘   
st                                                           └──────────────┘└───┘
279  
280  lemma summable_iff_summable_ne_zero_bij : summable f ↔ summable g :=
id                                             └──────┘   └──────┘ 
src                                            └──────┘    └──────┘
typ                                            └──────┘   └──────┘ 
doc                                            └──────┘     └──────┘
281  exists_congr $
id   └──────────┘
src  └──────────┘
typ  └──────────┘
282    assume a, has_sum_iff_has_sum_of_ne_zero_bij @i h₁ h₂ h₃
id              └────────────────────────────────┘   └┘ └┘ └┘
src              └────────────────────────────────┘
typ             └────────────────────────────────┘   └┘ └┘ └┘
283  
284  end has_sum_iff_has_sum_of_bij_ne_zero
285  
286  section tsum
287  variables [add_comm_monoid α] [topological_space α] [t2_space α]
id              └─────────────┘     └───────────────┘     └──────┘
src             └─────────────┘     └───────────────┘     └──────┘
typ             └─────────────┘     └───────────────┘     └──────┘
doc                                 └───────────────┘     └──────┘
288  variables {f g : β → α} {a a₁ a₂ : α}
289  
290  lemma has_sum_unique : has_sum f a₁ → has_sum f a₂ → a₁ = a₂ := tendsto_nhds_unique at_top_ne_bot
id                          └─────┘  └┘   └─────┘  └┘   └┘  └┘    └─────────────────┘ └───────────┘
src                         └─────┘        └─────┘                  └─────────────────┘ └───────────┘
typ                         └─────┘  └┘   └─────┘  └┘   └┘  └┘    └─────────────────┘ └───────────┘
doc                         └─────┘        └─────┘
291  
292  lemma tsum_eq_has_sum (ha : has_sum f a) : (∑b, f b) = a := has_sum_unique (has_sum_tsum ⟨a, ha⟩) ha
id                               └─────┘                └────────────┘  └──────────┘    └┘   └┘
src                              └─────┘                      └────────────┘  └──────────┘
typ                              └─────┘                └────────────┘  └──────────┘    └┘   └┘
doc                              └─────┘          
293  
294  lemma has_sum_iff_of_summable (h : summable f) : has_sum f a ↔ (∑b, f b) = a :=
id                                      └──────┘     └─────┘          
src                                     └──────┘      └─────┘              
typ                                     └──────┘     └─────┘          
doc                                     └──────┘      └─────┘         
295  iff.intro tsum_eq_has_sum (assume eq, eq ▸ has_sum_tsum h)
id   └───────┘ └─────────────┘         └┘  └┘  └──────────┘ 
src  └───────┘ └─────────────┘         └┘  └┘  └──────────┘
typ  └───────┘ └─────────────┘         └┘  └┘  └──────────┘ 
296  
297  @[simp] lemma tsum_zero : (∑b:β, 0:α) = 0 := tsum_eq_has_sum has_sum_zero
id                                           └─────────────┘ └──────────┘
src                                            └─────────────┘ └──────────┘
typ                                          └─────────────┘ └──────────┘
doc    └──┘                                                     └──────────┘
298  
299  lemma tsum_eq_sum {f : β → α} {s : finset β} (hf : ∀b∉s, f b = 0)  :
id                                    └────┘               
src                                     └────┘                    
typ                                   └────┘               
doc                                     └────┘
300    (∑b, f b) = s.sum f :=
id           └──┘ 
src              └──┘
typ          └──┘ 
doc      
301  tsum_eq_has_sum $ has_sum_sum_of_ne_finset_zero hf
id   └─────────────┘   └───────────────────────────┘ └┘
src  └─────────────┘   └───────────────────────────┘
typ  └─────────────┘   └───────────────────────────┘ └┘
doc                    └───────────────────────────┘
302  
303  lemma tsum_fintype [fintype β] (f : β → α) : (∑b, f b) = finset.univ.sum f :=
id                       └─────┘                     └─────────┘└──┘ 
src                      └─────┘                           └─────────┘└──┘
typ                      └─────┘                     └─────────┘└──┘ 
doc                      └─────┘                            └─────────┘
304  tsum_eq_has_sum $ has_sum_fintype f
id   └─────────────┘   └─────────────┘ 
src  └─────────────┘   └─────────────┘
typ  └─────────────┘   └─────────────┘ 
305  
306  lemma tsum_eq_single {f : β → α} (b : β) (hf : ∀b' ≠ b, f b' = 0)  :
id                                                └┘      └┘ 
src                                                               
typ                                               └┘      └┘ 
307    (∑b, f b) = f b :=
id            
src            
typ           
doc      
308  tsum_eq_has_sum $ has_sum_single b hf
id   └─────────────┘   └────────────┘  └┘
src  └─────────────┘   └────────────┘
typ  └─────────────┘   └────────────┘  └┘
309  
310  @[simp] lemma tsum_ite_eq (b : β) (a : α) : (∑b', if b' = b then a else 0) = a :=
id                                              └┘    └┘                  
src                                                                          
typ                                             └┘    └┘                  
doc    └──┘                                         
311  tsum_eq_has_sum (has_sum_ite_eq b a)
id   └─────────────┘  └────────────┘  
src  └─────────────┘  └────────────┘
typ  └─────────────┘  └────────────┘  
312  
313  lemma tsum_eq_tsum_of_has_sum_iff_has_sum {f : β → α} {g : γ → α}
id                                                               
typ                                                              
314    (h : ∀{a}, has_sum f a ↔ has_sum g a) : (∑b, f b) = (∑c, g c) :=
id               └─────┘    └─────┘               
src               └─────┘      └─────┘                   
typ              └─────┘    └─────┘               
doc               └─────┘       └─────┘                    
315  by_cases
id   └──────┘
src  └──────┘
typ  └──────┘
316    (assume : ∃a, has_sum f a,
id                └─────┘  
src                └─────┘
typ               └─────┘  
doc                  └─────┘
317      let ⟨a, hfa⟩ := this in
id       └─┘    └─┘     └──┘
typ      └─┘    └─┘     └──┘
318      have hga : has_sum g a, from h.mp hfa,
id                  └─────┘          └─┘
src                 └─────┘            └─┘
typ                 └─────┘          └─┘
doc                 └─────┘
319      by rw [tsum_eq_has_sum hfa, tsum_eq_has_sum hga])
id              └─────────────┘ └─┘  └─────────────┘ └─┘
src         └──┘└─────────────┘   └┘└─────────────┘   
typ         └──┘└─────────────┘└─┘└┘└─────────────┘└─┘
doc         └──┘                  └┘                  
txt         └──┘                  └┘                  
par         └──┘                  └┘                  
pid           └┘                  └┘                  
st         └──────────────────────┘└───────────────────┘
320    (assume hf : ¬ summable f,
id                   └──────┘ 
src                  └──────┘
typ                  └──────┘ 
doc                   └──────┘
321      have hg : ¬ summable g, from assume ⟨a, hga⟩, hf ⟨a, h.mpr hga⟩,
id                  └──────┘                 └─┘   └┘     └──┘
src                 └──────┘                                  └──┘
typ                 └──────┘                 └─┘   └┘     └──┘
doc                  └──────┘
322      by simp [tsum, hf, hg])
id                └──┘  └┘  └┘
src         └────┘└──┘└┘  └┘  
typ         └────┘└──┘└┘└┘└┘└┘
doc         └────┘└──┘└┘  └┘  
txt         └────┘    └┘  └┘  
par         └────┘    └┘  └┘  
pid                 └┘  └┘  
st         └──────────────────┘
323  
324  lemma tsum_eq_tsum_of_ne_zero {f : β → α} {g : γ → α}
id                                                   
typ                                                  
325    (i : Π⦃c⦄, g c ≠ 0 → β) (hi : ∀⦃c⦄ (h : g c ≠ 0), f (i h) ≠ 0)
id                                                   
src                                                            
typ                                                  
326    (j : Π⦃b⦄, f b ≠ 0 → γ) (hj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) ≠ 0)
id                                                   
src                                                            
typ                                                  
327    (hji : ∀⦃c⦄ (h : g c ≠ 0), j (hi h) = c)
id                              └┘    
src                                       
typ                             └┘    
328    (hij : ∀⦃b⦄ (h : f b ≠ 0), i (hj h) = b)
id                              └┘    
src                                       
typ                             └┘    
329    (hgj : ∀⦃b⦄ (h : f b ≠ 0), g (j h) = f b) :
id                                   
src                                      
typ                                  
330    (∑i, f i) = (∑j, g j) :=
id              
src               
typ             
doc                
331  tsum_eq_tsum_of_has_sum_iff_has_sum $ assume a, has_sum_iff_has_sum_of_ne_zero i hi j hj hji hij hgj
id   └─────────────────────────────────┘            └────────────────────────────┘  └┘  └┘ └─┘ └─┘ └─┘
src  └─────────────────────────────────┘             └────────────────────────────┘
typ  └─────────────────────────────────┘            └────────────────────────────┘  └┘  └┘ └─┘ └─┘ └─┘
332  
333  lemma tsum_eq_tsum_of_ne_zero_bij {f : β → α} {g : γ → α}
id                                                       
typ                                                      
334    (i : Π⦃c⦄, g c ≠ 0 → β)
id                      
src                   
typ                     
335    (h₁ : ∀⦃c₁ c₂⦄ (h₁ : g c₁ ≠ 0) (h₂ : g c₂ ≠ 0), i h₁ = i h₂ → c₁ = c₂)
id             └┘ └┘         └┘            └┘       └┘   └┘   └┘  └┘
src                                                                  
typ            └┘ └┘         └┘            └┘       └┘   └┘   └┘  └┘
336    (h₂ : ∀⦃b⦄, f b ≠ 0 → ∃c (h : g c ≠ 0), i h = b)
id                                      
src                                            
typ                                     
337    (h₃ : ∀⦃c⦄ (h : g c ≠ 0), f (i h) = g c) :
id                                  
src                                     
typ                                 
338    (∑i, f i) = (∑j, g j) :=
id              
src               
typ             
doc                
339  tsum_eq_tsum_of_has_sum_iff_has_sum $ assume a, has_sum_iff_has_sum_of_ne_zero_bij i h₁ h₂ h₃
id   └─────────────────────────────────┘            └────────────────────────────────┘  └┘ └┘ └┘
src  └─────────────────────────────────┘             └────────────────────────────────┘
typ  └─────────────────────────────────┘            └────────────────────────────────┘  └┘ └┘ └┘
340  
341  lemma tsum_eq_tsum_of_iso (j : γ → β) (i : β → γ)
id                                               
typ                                              
342    (h₁ : ∀x, i (j x) = x) (h₂ : ∀x, j (i x) = x) :
id                                     
src                                            
typ                                    
343    (∑c, f (j c)) = (∑b, f b) :=
id                 
src                   
typ                
doc                    
344  tsum_eq_tsum_of_has_sum_iff_has_sum $ assume a, has_sum_iff_has_sum_of_iso i h₁ h₂
id   └─────────────────────────────────┘            └────────────────────────┘  └┘ └┘
src  └─────────────────────────────────┘             └────────────────────────┘
typ  └─────────────────────────────────┘            └────────────────────────┘  └┘ └┘
345  
346  lemma tsum_equiv (j : γ ≃ β) : (∑c, f (j c)) = (∑b, f b) :=
id                                           
src                                               
typ                                          
doc                                                
347  tsum_eq_tsum_of_iso j j.symm (by simp) (by simp)
id   └─────────────────┘  └───┘
src  └─────────────────┘    └───┘     └──┘      └──┘
typ  └─────────────────┘  └───┘     └──┘      └──┘
doc                                   └──┘      └──┘
txt                                   └──┘      └──┘
par                                   └──┘      └──┘
st                                   └───┘     └───┘
348  
349  variable [topological_add_monoid α]
id             └────────────────────┘
src            └────────────────────┘
typ            └────────────────────┘
doc            └────────────────────┘
350  
351  lemma tsum_add (hf : summable f) (hg : summable g) : (∑b, f b + g b) = (∑b, f b) + (∑b, g b) :=
id                        └──────┘         └──────┘                       
src                       └──────┘          └──────┘                               
typ                       └──────┘         └──────┘                       
doc                       └──────┘          └──────┘                                  
352  tsum_eq_has_sum $ has_sum_add (has_sum_tsum hf) (has_sum_tsum hg)
id   └─────────────┘   └─────────┘  └──────────┘ └┘   └──────────┘ └┘
src  └─────────────┘   └─────────┘  └──────────┘      └──────────┘
typ  └─────────────┘   └─────────┘  └──────────┘ └┘   └──────────┘ └┘
353  
354  lemma tsum_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, summable (f i)) :
id                                    └────┘             └──────┘   
src                                      └────┘                └──────┘
typ                                   └────┘             └──────┘   
doc                                      └────┘                └──────┘
355    (∑b, s.sum (λi, f i b)) = s.sum (λi, ∑b, f i b) :=
id       └──┘           └──┘        
src        └──┘                └──┘       
typ      └──┘           └──┘        
doc                                        
356  tsum_eq_has_sum $ has_sum_sum $ assume i hi, has_sum_tsum $ hf i hi
id   └─────────────┘   └─────────┘           └┘  └──────────┘   └┘  └┘
src  └─────────────┘   └─────────┘                └──────────┘
typ  └─────────────┘   └─────────┘           └┘  └──────────┘   └┘  └┘
357  
358  lemma tsum_sigma [regular_space α] {γ : β → Type*} {f : (Σb:β, γ b) → α}
id                     └───────────┘                                
src                    └───────────┘                             
typ                    └───────────┘                                
doc                    └───────────┘
359    (h₁ : ∀b, summable (λc, f ⟨b, c⟩)) (h₂ : summable f) : (∑p, f p) = (∑b c, f ⟨b, c⟩) :=
id              └──────┘                   └──────┘                  
src              └──────┘                       └──────┘                   
typ             └──────┘                   └──────┘                  
doc              └──────┘                       └──────┘                    
360  (tsum_eq_has_sum $ has_sum_sigma (assume b, has_sum_tsum $ h₁ b) $ has_sum_tsum h₂).symm
id    └─────────────┘   └───────────┘           └──────────┘   └┘     └──────────┘ └┘ └──┘
src   └─────────────┘   └───────────┘            └──────────┘           └──────────┘    └──┘
typ   └─────────────┘   └───────────┘           └──────────┘   └┘     └──────────┘ └┘ └──┘
361  
362  end tsum
363  
364  section topological_group
365  variables [add_comm_group α] [topological_space α] [topological_add_group α]
id              └────────────┘     └───────────────┘     └───────────────────┘
src             └────────────┘     └───────────────┘     └───────────────────┘
typ             └────────────┘     └───────────────┘     └───────────────────┘
doc                                └───────────────┘     └───────────────────┘
366  variables {f g : β → α} {a a₁ a₂ : α}
367  
368  lemma has_sum_neg : has_sum f a → has_sum (λb, - f b) (- a) :=
id                       └─────┘     └─────┘           
src                      └─────┘       └─────┘             
typ                      └─────┘     └─────┘           
doc                      └─────┘       └─────┘
369  has_sum_hom has_neg.neg continuous_neg
id   └─────────┘ └─────────┘ └────────────┘
src  └─────────┘ └─────────┘ └────────────┘
typ  └─────────┘ └─────────┘ └────────────┘
370  
371  lemma summable_neg (hf : summable f) : summable (λb, - f b) :=
id                            └──────┘     └──────┘       
src                           └──────┘      └──────┘      
typ                           └──────┘     └──────┘       
doc                           └──────┘      └──────┘
372  summable_spec $ has_sum_neg $ has_sum_tsum $ hf
id   └───────────┘   └─────────┘   └──────────┘   └┘
src  └───────────┘   └─────────┘   └──────────┘
typ  └───────────┘   └─────────┘   └──────────┘   └┘
373  
374  lemma has_sum_sub (hf : has_sum f a₁) (hg : has_sum g a₂) : has_sum (λb, f b - g b) (a₁ - a₂) :=
id                           └─────┘  └┘        └─────┘  └┘    └─────┘            └┘  └┘
src                          └─────┘             └─────┘         └─────┘                    
typ                          └─────┘  └┘        └─────┘  └┘    └─────┘            └┘  └┘
doc                          └─────┘             └─────┘         └─────┘
375  by simp; exact has_sum_add hf (has_sum_neg hg)
id                  └─────────┘ └┘  └─────────┘ └┘
src     └──┘  └────┘└─────────┘   └─────────┘  └─
typ     └──┘  └────┘└─────────┘└┘ └─────────┘└┘└─
doc     └──┘  └────┘                           └─
txt     └──┘  └────┘                           └─
par     └──┘  └────┘                           └─
pid                                           
st     └────────────────────────────────────────────
376  
src  
typ  
doc  
txt  
par  
pid  
st   
377  lemma summable_sub (hf : summable f) (hg : summable g) : summable (λb, f b - g b) :=
id                            └──────┘         └──────┘     └──────┘         
src                           └──────┘          └──────┘      └──────┘          
typ                           └──────┘         └──────┘     └──────┘         
doc                           └──────┘          └──────┘      └──────┘
378  summable_spec $ has_sum_sub (has_sum_tsum hf) (has_sum_tsum hg)
id   └───────────┘   └─────────┘  └──────────┘ └┘   └──────────┘ └┘
src  └───────────┘   └─────────┘  └──────────┘      └──────────┘
typ  └───────────┘   └─────────┘  └──────────┘ └┘   └──────────┘ └┘
379  
380  section tsum
381  variables [t2_space α]
id              └──────┘
src             └──────┘
typ             └──────┘
doc             └──────┘
382  
383  lemma tsum_neg (hf : summable f) : (∑b, - f b) = - (∑b, f b) :=
id                        └──────┘                
src                       └──────┘                   
typ                       └──────┘                
doc                       └──────┘                      
384  tsum_eq_has_sum $ has_sum_neg $ has_sum_tsum $ hf
id   └─────────────┘   └─────────┘   └──────────┘   └┘
src  └─────────────┘   └─────────┘   └──────────┘
typ  └─────────────┘   └─────────┘   └──────────┘   └┘
385  
386  lemma tsum_sub (hf : summable f) (hg : summable g) : (∑b, f b - g b) = (∑b, f b) - (∑b, g b) :=
id                        └──────┘         └──────┘                       
src                       └──────┘          └──────┘                               
typ                       └──────┘         └──────┘                       
doc                       └──────┘          └──────┘                                  
387  tsum_eq_has_sum $ has_sum_sub (has_sum_tsum hf) (has_sum_tsum hg)
id   └─────────────┘   └─────────┘  └──────────┘ └┘   └──────────┘ └┘
src  └─────────────┘   └─────────┘  └──────────┘      └──────────┘
typ  └─────────────┘   └─────────┘  └──────────┘ └┘   └──────────┘ └┘
388  
389  lemma tsum_eq_zero_add {f : ℕ → α} (hf : summable f) : (∑b, f b) = f 0 + (∑b, f (b + 1)) :=
id                                          └──────┘                    
src                                          └──────┘                            
typ                                         └──────┘                    
doc                                           └──────┘                        
390  begin
st   └─────
391    let f₁ : ℕ → α := λ n, nat.rec (f 0) (λ _ _, 0) n,
id                           └─────┘  
src    └───────┘   └──┘ └──┘└─────┘  └──┘  └───────┘
typ    └───────┘  └──┘ └──┘└─────┘ └──┘  └───────┘
doc    └───────┘   └──┘ └──┘         └──┘  └───────┘
txt    └───────┘   └──┘ └──┘         └──┘  └───────┘
par    └───────┘   └──┘ └──┘         └──┘  └───────┘
pid    └────┘└─┘   └──┘ └──┘         └──┘  └───────┘
st   ──────────────────────────────────────────────────┘└─
392    let f₂ : ℕ → α := λ n, nat.rec 0 (λ k _, f (k+1)) n,
id                           └─────┘              
src    └───────┘   └──┘ └──┘└─────┘└─┘  └────┘   └──┘
typ    └───────┘  └──┘ └──┘└─────┘└─┘  └────┘  └──┘
doc    └───────┘   └──┘ └──┘       └─┘  └────┘    └──┘
txt    └───────┘   └──┘ └──┘       └─┘  └────┘    └──┘
par    └───────┘   └──┘ └──┘       └─┘  └────┘    └──┘
pid    └────┘└─┘   └──┘ └──┘       └─┘  └────┘    └──┘
st   ────────────────────────────────────────────────────┘└─
393    have : f = λ n, f₁ n + f₂ n, { ext n, symmetry, cases n, apply add_zero, apply zero_add },
id                   └┘     └┘                                     └──────┘        └──────┘
src    └─────┘  └──┘           └───┘  └──────┘  └────┘   └────┘└──────┘  └────┘└──────┘
typ    └─────┘ └──┘└┘  └┘     └───┘  └──────┘  └────┘  └────┘└──────┘  └────┘└──────┘
doc    └─────┘   └──┘           └───┘  └──────┘  └────┘   └────┘          └────┘        
txt    └─────┘   └──┘           └───┘  └──────┘  └────┘   └────┘          └────┘        
par    └─────┘   └──┘           └───┘  └──────┘  └────┘   └────┘          └────┘        
pid    └───┘└┘   └──┘              └┘                                                
st   ────────────────────────────┘└──┘└───┘└────────┘└───────┘└──────────────┘└───────────────┘└┘
394    have hf₁ : summable f₁,
id                └──────┘ └┘
src    └─────────┘└──────┘
typ    └─────────┘└──────┘└┘
doc    └─────────┘└──────┘
txt    └─────────┘        
par    └─────────┘        
pid    └──────┘└─┘        
st   ───────────────────────┘└─
395    { fapply summable_sum_of_ne_finset_zero,
id              └────────────────────────────┘
src      └─────┘└────────────────────────────┘
typ      └─────┘└────────────────────────────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid            
st   ───┘└───────────────────────────────────┘└─
396      { exact finset.singleton 0 },
id               └──────────────┘
src        └────┘└──────────────┘└─┘
typ        └────┘└──────────────┘└─┘
doc        └────┘└──────────────┘└─┘
txt        └────┘                └─┘
par        └────┘                └─┘
pid                             └┘
st   ─────┘└───────────────────────┘└┘
397      { rintros (_ | n) hn,
src        └────────────────┘
typ        └────────────────┘
doc        └────────────────┘
txt        └────────────────┘
par        └────────────────┘
pid               └─────────┘
st   ───────────────────────┘└─
398        { exfalso,
src          └─────┘
typ          └─────┘
doc          └─────┘
txt          └─────┘
par          └─────┘
st   ───────┘└─────┘└─
399          apply hn,
src          └────┘
typ          └────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ───────────────┘└─
400          apply finset.mem_singleton_self },
id                 └───────────────────────┘
src          └────┘└───────────────────────┘
typ          └────┘└───────────────────────┘
doc          └────┘                         
txt          └────┘                         
par          └────┘                         
pid                                        
st   ───────────────────────────────────────┘└┘
401        { refl } } },
src          └───┘
typ          └───┘
doc          └───┘
txt          └───┘
par          └───┘
pid              
st   ────────────┘└────┘
402    have hf₂ : summable f₂,
id                └──────┘ └┘
src    └─────────┘└──────┘
typ    └─────────┘└──────┘└┘
doc    └─────────┘└──────┘
txt    └─────────┘        
par    └─────────┘        
pid    └──────┘└─┘        
st   ───────────────────────┘└─
403    { have : f₂ = λ n, f n - f₁ n, ext, rw [eq_sub_iff_add_eq', this],
id              └┘            └┘             └────────────────┘  └──┘
src      └─────┘    └──┘       └─┘  └──┘└────────────────┘└┘    
typ      └─────┘└┘  └──┘ └┘   └─┘  └──┘└────────────────┘└┘└──┘
doc      └─────┘    └──┘        └─┘  └──┘                  └┘    
txt      └─────┘    └──┘        └─┘  └──┘                  └┘    
par      └─────┘    └──┘        └─┘  └──┘                  └┘    
pid      └───┘└┘    └──┘               └┘                  └┘    
st   ───┘└─────────────────────────┘└───┘└──────────────────────┘└────┘└──
404      rw [this], apply summable_sub hf hf₁ },
id           └──┘         └──────────┘ └┘ └─┘
src      └──┘      └────┘└──────────┘     
typ      └──┘└──┘  └────┘└──────────┘└┘└─┘
doc      └──┘      └────┘                 
txt      └──┘      └────┘                 
par      └──┘      └────┘                 
pid        └┘                            
st   ───────────┘└───────────────────────────┘└┘
405    conv_lhs { rw [this] },
id                    └──┘
src    └─────────┘└──┘    └┘
typ    └─────────┘└──┘└──┘└┘
txt    └─────────┘└──┘    └┘
par    └─────────┘└──┘    └┘
pid            └────┘    └─┘
st   ───────────┘└───────┘ └┘
406    rw [tsum_add hf₁ hf₂, tsum_eq_single 0],
id         └──────┘ └─┘ └─┘  └────────────┘
src    └──┘└──────┘      └┘└────────────┘└─┘
typ    └──┘└──────┘└─┘└─┘└┘└────────────┘└─┘
doc    └──┘              └┘              └─┘
txt    └──┘              └┘              └─┘
par    └──┘              └┘              └─┘
pid      └┘              └┘              └─┘
st   ─────────────────────┘└───────────────┘└───
407    { congr' 1,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid            
st   ───┘└──────┘└─
408      fapply tsum_eq_tsum_of_ne_zero_bij (λ n _, n + 1),
id              └─────────────────────────┘
src      └─────┘└─────────────────────────┘  └────┘  └─┘
typ      └─────┘└─────────────────────────┘  └────┘  └─┘
doc      └─────┘                             └────┘  └─┘
txt      └─────┘                             └────┘  └─┘
par      └─────┘                             └────┘  └─┘
pid                                         └────┘  └─┘
st   ────────────────────────────────────────────────────┘└─
409      { intros _ _ _ _, exact nat.succ_inj },
id                               └──────────┘
src        └────────────┘  └────┘└──────────┘
typ        └────────────┘  └────┘└──────────┘
doc        └────────────┘  └────┘            
txt        └────────────┘  └────┘            
par        └────────────┘  └────┘            
pid              └──────┘                   
st   ─────┘└────────────┘└───────────────────┘└┘
410      { rintros (_ | n) h,
src        └───────────────┘
typ        └───────────────┘
doc        └───────────────┘
txt        └───────────────┘
par        └───────────────┘
pid               └────────┘
st   ─────┘└───────────────┘└─
411        { contradiction },
src          └────────────┘
typ          └────────────┘
doc          └────────────┘
txt          └────────────┘
par          └────────────┘
pid                       
st   ───────┘└────────────┘└┘
412        { exact ⟨n, h, rfl⟩ } },
id                      └─┘
src          └────┘  └┘ └┘└─┘└┘
typ          └────┘ └┘└┘└─┘└┘
doc          └────┘  └┘ └┘   └┘
txt          └────┘  └┘ └┘   └┘
par          └────┘  └┘ └┘   └┘
pid                 └┘ └┘   
st   ─────────────────────────┘└──┘
413      { intros, refl },
src        └────┘  └───┘
typ        └────┘  └───┘
doc        └────┘  └───┘
txt        └────┘  └───┘
par        └────┘  └───┘
pid                    
st   ─────┘└────┘└─────┘└┘
414      { apply_instance } },
src        └─────────────┘
typ        └─────────────┘
doc        └─────────────┘
txt        └─────────────┘
par        └─────────────┘
pid                      
st   ────────────────────┘└──┘
415    { rintros (_ | n) hn,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid             └─────────┘
st   ───┘└────────────────┘└─
416      { contradiction },
src        └────────────┘
typ        └────────────┘
doc        └────────────┘
txt        └────────────┘
par        └────────────┘
pid                     
st   ─────┘└────────────┘└┘
417      { refl } },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└──┘
418    { apply_instance }
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid                    
st   ──────────────────┘└─
419  end
st   ──┘
420  
421  end tsum
422  
423  end topological_group
424  
425  section topological_semiring
426  variables [semiring α] [topological_space α] [topological_semiring α]
id              └──────┘     └───────────────┘     └──────────────────┘
src             └──────┘     └───────────────┘     └──────────────────┘
typ             └──────┘     └───────────────┘     └──────────────────┘
doc                          └───────────────┘     └──────────────────┘
427  variables {f g : β → α} {a a₁ a₂ : α}
428  
429  lemma has_sum_mul_left (a₂) : has_sum f a₁ → has_sum (λb, a₂ * f b) (a₂ * a₁) :=
id                                 └─────┘  └┘   └─────┘     └┘      └┘  └┘
src                                └─────┘        └─────┘                   
typ                                └─────┘  └┘   └─────┘     └┘      └┘  └┘
doc                                └─────┘        └─────┘
430  has_sum_hom _ (continuous_const.mul continuous_id)
id   └─────────┘    └──────────────┘└──┘ └───────────┘
src  └─────────┘    └──────────────┘└──┘ └───────────┘
typ  └─────────┘    └──────────────┘└──┘ └───────────┘
431  
432  lemma has_sum_mul_right (a₂) (hf : has_sum f a₁) : has_sum (λb, f b * a₂) (a₁ * a₂) :=
id                                      └─────┘  └┘    └─────┘        └┘   └┘  └┘
src                                     └─────┘         └─────┘                   
typ                                     └─────┘  └┘    └─────┘        └┘   └┘  └┘
doc                                     └─────┘         └─────┘
433  @has_sum_hom _ _ _ _ _ f a₁ (λa, a * a₂) _ _ _
id    └─────────┘            └┘       └┘
src   └─────────┘                       
typ   └─────────┘            └┘       └┘
434    (continuous_id.mul continuous_const) hf
id      └───────────┘└──┘ └──────────────┘  └┘
src     └───────────┘└──┘ └──────────────┘
typ     └───────────┘└──┘ └──────────────┘  └┘
435  
436  lemma summable_mul_left (a) (hf : summable f) : summable (λb, a * f b) :=
id                                     └──────┘     └──────┘        
src                                    └──────┘      └──────┘        
typ                                    └──────┘     └──────┘        
doc                                    └──────┘      └──────┘
437  summable_spec $ has_sum_mul_left _ $ has_sum_tsum hf
id   └───────────┘   └──────────────┘     └──────────┘ └┘
src  └───────────┘   └──────────────┘     └──────────┘
typ  └───────────┘   └──────────────┘     └──────────┘ └┘
438  
439  lemma summable_mul_right (a) (hf : summable f) : summable (λb, f b * a) :=
id                                      └──────┘     └──────┘        
src                                     └──────┘      └──────┘          
typ                                     └──────┘     └──────┘        
doc                                     └──────┘      └──────┘
440  summable_spec $ has_sum_mul_right _ $ has_sum_tsum hf
id   └───────────┘   └───────────────┘     └──────────┘ └┘
src  └───────────┘   └───────────────┘     └──────────┘
typ  └───────────┘   └───────────────┘     └──────────┘ └┘
441  
442  section tsum
443  variables [t2_space α]
id              └──────┘
src             └──────┘
typ             └──────┘
doc             └──────┘
444  
445  lemma tsum_mul_left (a) (hf : summable f) : (∑b, a * f b) = a * (∑b, f b) :=
id                                 └──────┘                  
src                                └──────┘                       
typ                                └──────┘                  
doc                                └──────┘                          
446  tsum_eq_has_sum $ has_sum_mul_left _ $ has_sum_tsum hf
id   └─────────────┘   └──────────────┘     └──────────┘ └┘
src  └─────────────┘   └──────────────┘     └──────────┘
typ  └─────────────┘   └──────────────┘     └──────────┘ └┘
447  
448  lemma tsum_mul_right (a) (hf : summable f) : (∑b, f b * a) = (∑b, f b) * a :=
id                                  └──────┘                   
src                                 └──────┘                          
typ                                 └──────┘                   
doc                                 └──────┘                      
449  tsum_eq_has_sum $ has_sum_mul_right _ $ has_sum_tsum hf
id   └─────────────┘   └───────────────┘     └──────────┘ └┘
src  └─────────────┘   └───────────────┘     └──────────┘
typ  └─────────────┘   └───────────────┘     └──────────┘ └┘
450  
451  end tsum
452  
453  end topological_semiring
454  
455  section order_topology
456  variables [ordered_comm_monoid α] [topological_space α] [order_closed_topology α]
id             └─────────────────┘    └───────────────┘     └───────────────────┘
src             └─────────────────┘     └───────────────┘     └───────────────────┘
typ            └─────────────────┘    └───────────────┘     └───────────────────┘
doc             └─────────────────┘     └───────────────┘     └───────────────────┘
457  variables {f g : β → α} {a a₁ a₂ : α}
458  
459  lemma has_sum_le (h : ∀b, f b ≤ g b) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ :=
id                                        └─────┘  └┘        └─────┘  └┘    └┘  └┘
src                                            └─────┘             └─────┘            
typ                                       └─────┘  └┘        └─────┘  └┘    └┘  └┘
doc                                             └─────┘             └─────┘
460  le_of_tendsto_of_tendsto at_top_ne_bot hf hg $ univ_mem_sets' $
id   └──────────────────────┘ └───────────┘ └┘ └┘   └────────────┘
src  └──────────────────────┘ └───────────┘         └────────────┘
typ  └──────────────────────┘ └───────────┘ └┘ └┘   └────────────┘
461    assume s, sum_le_sum $ assume b _, h b
id              └────────┘              
src              └────────┘
typ             └────────┘              
462  
463  lemma has_sum_le_inj {g : γ → α} (i : β → γ) (hi : injective i) (hs : ∀c∉set.range i, 0 ≤ g c)
id                                                  └───────┘           └───────┘       
src                                                     └───────┘             └───────┘      
typ                                                 └───────┘           └───────┘       
doc                                                                           └───────┘
464    (h : ∀b, f b ≤ g (i b)) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ :=
id                            └─────┘  └┘        └─────┘  └┘    └┘  └┘
src                                 └─────┘             └─────┘            
typ                           └─────┘  └┘        └─────┘  └┘    └┘  └┘
doc                                  └─────┘             └─────┘
465  have has_sum (λc, (partial_inv i c).cases_on' 0 f) a₁,
id        └─────┘      └─────────┘   └───────┘      └┘
src       └─────┘       └─────────┘     └───────┘
typ       └─────┘      └─────────┘   └───────┘      └┘
doc       └─────┘       └─────────┘
466  begin
st   └─────
467    refine (has_sum_iff_has_sum_of_ne_zero_bij (λb _, i b) _ _ _).2 hf,
id             └────────────────────────────────┘                     └┘
src    └─────┘ └────────────────────────────────┘  └───┘  └─────────┘
typ    └─────┘ └────────────────────────────────┘  └───┘ └─────────┘└┘
doc    └─────┘                                     └───┘  └─────────┘
txt    └─────┘                                     └───┘  └─────────┘
par    └─────┘                                     └───┘  └─────────┘
pid                                               └───┘  └─────────┘
st   ───────────────────────────────────────────────────────────────────┘└─
468    { assume c₁ c₂ h₁ h₂ eq, exact hi eq },
id                                    └┘ └┘
src      └───────────────────┘  └────┘  └┘
typ      └───────────────────┘  └────┘└┘└┘
doc      └───────────────────┘  └────┘    
txt      └───────────────────┘  └────┘    
par      └───────────────────┘  └────┘    
pid      └───────────────────┘           
st   ───┘└───────────────────┘└────────────┘└┘
469    { assume c hc,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
470      cases eq : partial_inv i c with b; rw eq at hc,
id                  └─────────┘              └┘
src      └────┘  └─┘└─────────┘  └─────┘  └─┘└┘└────┘
typ      └────┘  └─┘└─────────┘└─────┘  └─┘└┘└────┘
doc      └────┘  └─┘└─────────┘  └─────┘  └─┘  └────┘
txt      └────┘  └─┘             └─────┘  └─┘  └────┘
par      └────┘  └─┘             └─────┘  └─┘  └────┘
pid             └─┘             └─────┘      └────┘
st   ─────────────────────────────────────────┘└┘└────┘└─
471      { contradiction },
src        └────────────┘
typ        └────────────┘
doc        └────────────┘
txt        └────────────┘
par        └────────────┘
pid                     
st   ─────┘└────────────┘└┘
472      { rw [partial_inv_of_injective hi] at eq,
id             └──────────────────────┘ └┘
src        └──┘└──────────────────────┘  └─────┘
typ        └──┘└──────────────────────┘└┘└─────┘
doc        └──┘                          └─────┘
txt        └──┘                          └─────┘
par        └──┘                          └─────┘
pid          └┘                          └────┘
st   ────────────────────────────────────┘└────┘└─
473        exact ⟨b, hc, eq⟩ } },
id                  └┘  └┘
src        └────┘  └┘  └┘└┘└┘
typ        └────┘ └┘└┘└┘└┘└┘
doc        └────┘  └┘  └┘  └┘
txt        └────┘  └┘  └┘  └┘
par        └────┘  └┘  └┘  └┘
pid               └┘  └┘  
st   ───────────────────────┘└──┘
474    { assume c hc, rw [partial_inv_left hi, option.cases_on'] }
id                        └──────────────┘ └┘  └──────────────┘
src      └─────────┘  └──┘└──────────────┘  └┘└──────────────┘└┘
typ      └─────────┘  └──┘└──────────────┘└┘└┘└──────────────┘└┘
doc      └─────────┘  └──┘                  └┘                └┘
txt      └─────────┘  └──┘                  └┘                └┘
par      └─────────┘  └──┘                  └┘                └┘
pid      └─────────┘    └┘                  └┘                
st   ──────────────┘└───────────────────────┘└────────────────┘└─
475  end,
st   ──┘
476  begin
st   └─────
477    refine has_sum_le (assume c, _) this hg,
id            └────────┘               └──┘ └┘
src    └─────┘└────────┘       └─────┘    
typ    └─────┘└────────┘       └─────┘└──┘└┘
doc    └─────┘                 └─────┘    
txt    └─────┘                 └─────┘    
par    └─────┘                 └─────┘    
pid                           └─────┘    
st   ────────────────────────────────────────┘└─
478    by_cases c ∈ set.range i,
id                └───────┘ 
src    └───────┘ └───────┘
typ    └───────┘└───────┘
doc    └───────┘  └───────┘
txt    └───────┘           
par    └───────┘           
pid                       
st   ─────────────────────────┘└─
479    { rcases h with ⟨b, rfl⟩,
id              
src      └─────┘ └────────────┘
typ      └─────┘└────────────┘
doc      └─────┘ └────────────┘
txt      └─────┘ └────────────┘
par      └─────┘ └────────────┘
pid             └────────────┘
st   ───┘└────────────────────┘└─
480      rw [partial_inv_left hi, option.cases_on'],
id           └──────────────┘ └┘  └──────────────┘
src      └──┘└──────────────┘  └┘└──────────────┘
typ      └──┘└──────────────┘└┘└┘└──────────────┘
doc      └──┘                  └┘                
txt      └──┘                  └┘                
par      └──┘                  └┘                
pid        └┘                  └┘                
st   ──────────────────────────┘└────────────────┘└──
481      exact h _ },
id             
src      └────┘ └─┘
typ      └────┘└─┘
doc      └────┘ └─┘
txt      └────┘ └─┘
par      └────┘ └─┘
pid            └┘
st   ─────────────┘└┘
482    { have : partial_inv i c = none := dif_neg h,
id              └─────────┘     └──┘    └─────┘ 
src      └─────┘└─────────┘   └──┘└──┘└─────┘
typ      └─────┘└─────────┘ └──┘└──┘└─────┘
doc      └─────┘└─────────┘       └──┘       
txt      └─────┘                  └──┘       
par      └─────┘                  └──┘       
pid      └───┘└┘                  └──┘       
st   ─────────────────────────────────────────────┘└─
483      rw [this, option.cases_on'],
id           └──┘  └──────────────┘
src      └──┘    └┘└──────────────┘
typ      └──┘└──┘└┘└──────────────┘
doc      └──┘    └┘                
txt      └──┘    └┘                
par      └──┘    └┘                
pid        └┘    └┘                
st   ───────────┘└────────────────┘└──
484      exact hs _ h }
id             └┘   
src      └────┘  └─┘ 
typ      └────┘└┘└─┘
doc      └────┘  └─┘ 
txt      └────┘  └─┘ 
par      └────┘  └─┘ 
pid             └─┘ 
st   ────────────────┘└─
485  end
st   ──┘
486  
487  lemma sum_le_has_sum {f : β → α} (s : finset β) (hs : ∀ b∉s, 0 ≤ f b) (hf : has_sum f a) :
id                                       └────┘                          └─────┘  
src                                        └────┘                               └─────┘
typ                                      └────┘                          └─────┘  
doc                                        └────┘                                └─────┘
488    s.sum f ≤ a :=
id     └──┘   
src     └──┘   
typ    └──┘   
489  ge_of_tendsto at_top_ne_bot hf (mem_at_top_sets.2 ⟨s, λ t hst,
id   └───────────┘ └───────────┘ └┘  └─────────────┘        └─┘
src  └───────────┘ └───────────┘     └─────────────┘
typ  └───────────┘ └───────────┘ └┘  └─────────────┘        └─┘
490    sum_le_sum_of_subset_of_nonneg hst $ λ b hbt hbs, hs b hbs⟩)
id     └────────────────────────────┘ └─┘      └─┘ └─┘  └┘  └─┘
src    └────────────────────────────┘
typ    └────────────────────────────┘ └─┘      └─┘ └─┘  └┘  └─┘
491  
492  lemma sum_le_tsum {f : β → α} (s : finset β) (hs : ∀ b∉s, 0 ≤ f b) (hf : summable f) :
id                                    └────┘                          └──────┘ 
src                                     └────┘                               └──────┘
typ                                   └────┘                          └──────┘ 
doc                                     └────┘                                └──────┘
493    s.sum f ≤ tsum f :=
id     └──┘   └──┘ 
src     └──┘    └──┘
typ    └──┘   └──┘ 
doc              └──┘
494  sum_le_has_sum s hs (has_sum_tsum hf)
id   └────────────┘  └┘  └──────────┘ └┘
src  └────────────┘       └──────────┘
typ  └────────────┘  └┘  └──────────┘ └┘
495  
496  lemma tsum_le_tsum (h : ∀b, f b ≤ g b) (hf : summable f) (hg : summable g) : (∑b, f b) ≤ (∑b, g b) :=
id                                          └──────┘         └──────┘              
src                                              └──────┘          └──────┘                 
typ                                         └──────┘         └──────┘              
doc                                               └──────┘          └──────┘                  
497  has_sum_le h (has_sum_tsum hf) (has_sum_tsum hg)
id   └────────┘   └──────────┘ └┘   └──────────┘ └┘
src  └────────┘    └──────────┘      └──────────┘
typ  └────────┘   └──────────┘ └┘   └──────────┘ └┘
498  
499  end order_topology
500  
501  section uniform_group
502  
503  variables [add_comm_group α] [uniform_space α] [complete_space α]
id              └────────────┘    └───────────┘     └────────────┘
src             └────────────┘     └───────────┘     └────────────┘
typ             └────────────┘    └───────────┘     └────────────┘
doc                                └───────────┘     └────────────┘
504  variables (f g : β → α) {a a₁ a₂ : α}
505  
506  lemma summable_iff_cauchy : summable f ↔ cauchy (map (λ (s : finset β), sum s f) at_top) :=
id                               └──────┘   └────┘  └─┘         └────┘    └─┘    └────┘
src                              └──────┘    └────┘  └─┘         └────┘     └─┘      └────┘
typ                              └──────┘   └────┘  └─┘         └────┘    └─┘    └────┘
doc                              └──────┘     └────┘  └─┘         └────┘              └────┘
507  (cauchy_map_iff_exists_tendsto at_top_ne_bot).symm
id    └───────────────────────────┘ └───────────┘ └──┘
src   └───────────────────────────┘ └───────────┘ └──┘
typ   └───────────────────────────┘ └───────────┘ └──┘
508  
509  variable [uniform_add_group α]
id             └───────────────┘
src            └───────────────┘
typ            └───────────────┘
doc            └───────────────┘
510  
511  lemma summable_iff_vanishing :
512    summable f ↔ ∀ e ∈ 𝓝 (0:α), (∃s:finset β, ∀t, disjoint t s → t.sum f ∈ e) :=
id     └──────┘                  └────┘     └──────┘     └──┘   
src    └──────┘                     └────┘       └──────┘        └──┘   
typ    └──────┘                  └────┘     └──────┘     └──┘   
doc    └──────┘                       └────┘        └──────┘
513  begin
st   └─────
514    simp only [summable_iff_cauchy, cauchy_map_iff, and_iff_right at_top_ne_bot,
id                └─────────────────┘  └────────────┘  └───────────┘ └───────────┘
src    └─────────┘└─────────────────┘└┘└────────────┘└┘└───────────┘└───────────┘└─
typ    └─────────┘└─────────────────┘└┘└────────────┘└┘└───────────┘└───────────┘└─
doc    └─────────┘                   └┘              └┘                          └─
txt    └─────────┘                   └┘              └┘                          └─
par    └─────────┘                   └┘              └┘                          └─
pid        └──┘└┘                   └┘              └┘                          └─
st   ───────────────────────────────────────────────────────────────────────────────
515      prod_at_top_at_top_eq, uniformity_eq_comap_nhds_zero α, tendsto_comap_iff, (∘)],
id       └───────────────────┘  └───────────────────────────┘   └───────────────┘  
src  ───┘└───────────────────┘└┘└───────────────────────────┘ └┘└───────────────┘└┘└─┘
typ  ───┘└───────────────────┘└┘└───────────────────────────┘└┘└───────────────┘└┘└─┘
doc  ───┘                     └┘                              └┘                 └┘ └─┘
txt  ───┘                     └┘                              └┘                 └┘ └─┘
par  ───┘                     └┘                              └┘                 └┘ └─┘
pid  ───┘                     └┘                              └┘                 └┘ └─┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
516    rw [tendsto_at_top' (_ : finset β × finset β → α)],
id         └─────────────┘                └────┘    
src    └──┘└─────────────┘ └──┘       └────┘   └┘
typ    └──┘└─────────────┘ └──┘       └────┘ └┘
doc    └──┘                └──┘        └────┘   └┘
txt    └──┘                └──┘                 └┘
par    └──┘                └──┘                 └┘
pid      └┘                └──┘                 └┘
st   ──────────────────────────────────────────────────┘└──
517    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
518    { assume h e he,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid      └───────────┘
st   ───┘└───────────┘└─
519      rcases h e he with ⟨⟨s₁, s₂⟩, h⟩,
id                └┘
src      └─────┘    └─────────────────┘
typ      └─────┘└┘└─────────────────┘
doc      └─────┘    └─────────────────┘
txt      └─────┘    └─────────────────┘
par      └─────┘    └─────────────────┘
pid                └─────────────────┘
st   ───────────────────────────────────┘└─
520      use [s₁ ∪ s₂],
id            └┘  └┘
src      └───┘    
typ      └───┘└┘└┘
doc      └───┘     
txt      └───┘     
par      └───┘     
pid         └┘     
st   ────────────────┘└─
521      assume t ht,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
522      specialize h (s₁ ∪ s₂, (s₁ ∪ s₂) ∪ t) ⟨le_sup_left, le_sup_left_of_le le_sup_right⟩,
id                             └┘   └┘       └─────────┘  └───────────────┘ └──────────┘
src      └─────────┘      └┘      └┘  └┘ └─────────┘└┘└───────────────┘└──────────┘
typ      └─────────┘     └┘ └┘ └┘└┘ └┘ └─────────┘└┘└───────────────┘└──────────┘
doc      └─────────┘       └┘      └┘  └┘            └┘                             
txt      └─────────┘       └┘      └┘  └┘            └┘                             
par      └─────────┘       └┘      └┘  └┘            └┘                             
pid                       └┘      └┘  └┘            └┘                             
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
523      simpa only [finset.sum_union ht.symm, add_sub_cancel'] using h },
id                   └──────────────┘ └─────┘  └─────────────┘        
src      └──────────┘└──────────────┘└─────┘└┘└─────────────┘└──────┘ 
typ      └──────────┘└──────────────┘└─────┘└┘└─────────────┘└──────┘
doc      └──────────┘                       └┘               └──────┘ 
txt      └──────────┘                       └┘               └──────┘ 
par      └──────────┘                       └┘               └──────┘ 
pid           └──┘└┘                       └┘               └────┘ 
st   ──────────────────────────────────────────────────────────────────┘└┘
524    { assume h e he,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid      └───────────┘
st   ────────────────┘└─
525      rcases exists_nhds_half_neg he with ⟨d, hd, hde⟩,
id              └──────────────────┘ └┘
src      └─────┘└──────────────────┘  └────────────────┘
typ      └─────┘└──────────────────┘└┘└────────────────┘
doc      └─────┘                      └────────────────┘
txt      └─────┘                      └────────────────┘
par      └─────┘                      └────────────────┘
pid                                  └────────────────┘
st   ───────────────────────────────────────────────────┘└─
526      rcases h d hd with ⟨s, h⟩,
id                └┘
src      └─────┘    └──────────┘
typ      └─────┘└┘└──────────┘
doc      └─────┘    └──────────┘
txt      └─────┘    └──────────┘
par      └─────┘    └──────────┘
pid                └──────────┘
st   ────────────────────────────┘└─
527      use [(s, s)],
id                
src      └───┘  └┘ └┘
typ      └───┘  └┘└┘
doc      └───┘  └┘ └┘
txt      └───┘  └┘ └┘
par      └───┘  └┘ └┘
pid         └┘  └┘ └┘
st   ───────────────┘└─
528      rintros ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩,
src      └─────────────────────────┘
typ      └─────────────────────────┘
doc      └─────────────────────────┘
txt      └─────────────────────────┘
par      └─────────────────────────┘
pid             └──────────────────┘
st   ──────────────────────────────┘└─
529      have : t₂.sum f - t₁.sum f = (t₂ \ s).sum f - (t₁ \ s).sum f,
id              └────┘    └────┘     └┘              └┘         
src      └─────┘└────┘ └────┘     └────┘       └────┘
typ      └─────┘└────┘ └────┘  └┘ └────┘   └┘ └────┘
doc      └─────┘                     └────┘       └────┘
txt      └─────┘                     └────┘       └────┘
par      └─────┘                     └────┘       └────┘
pid      └───┘└┘                     └────┘       └────┘
st   ───────────────────────────────────────────────────────────────┘└─
530      { simp only [(finset.sum_sdiff ht₁).symm, (finset.sum_sdiff ht₂).symm,
id                     └──────────────┘ └─┘         └──────────────┘ └─┘
src        └─────────┘ └──────────────┘   └──────┘ └──────────────┘   └───────
typ        └─────────┘ └──────────────┘└─┘└──────┘ └──────────────┘└─┘└───────
doc        └─────────┘                    └──────┘                    └───────
txt        └─────────┘                    └──────┘                    └───────
par        └─────────┘                    └──────┘                    └───────
pid            └──┘└┘                    └──────┘                    └───────
st   ─────┘└────────────────────────────────────────────────────────────────────
531          add_sub_add_right_eq_sub] },
id           └──────────────────────┘
src  ───────┘└──────────────────────┘└┘
typ  ───────┘└──────────────────────┘└┘
doc  ───────┘                        └┘
txt  ───────┘                        └┘
par  ───────┘                        └┘
pid  ───────┘                        
st   ─────────────────────────────────┘└┘
532      simp only [this],
id                  └──┘
src      └─────────┘    
typ      └─────────┘└──┘
doc      └─────────┘    
txt      └─────────┘    
par      └─────────┘    
pid          └──┘└┘    
st   ───────────────────┘└─
533      exact hde _ _ (h _ finset.sdiff_disjoint) (h _ finset.sdiff_disjoint) }
id             └─┘                                     └───────────────────┘
src      └────┘   └───┘  └─┘                     └┘  └─┘└───────────────────┘└┘
typ      └────┘└─┘└───┘  └─┘                     └┘ └─┘└───────────────────┘└┘
doc      └────┘   └───┘  └─┘                     └┘  └─┘                     └┘
txt      └────┘   └───┘  └─┘                     └┘  └─┘                     └┘
par      └────┘   └───┘  └─┘                     └┘  └─┘                     └┘
pid              └───┘  └─┘                     └┘  └─┘                     
st   ─────────────────────────────────────────────────────────────────────────┘└─
534  end
st   ──┘
535  
536  /- TODO: generalize to monoid with a uniform continuous subtraction operator: `(a + b) - b = a` -/
537  lemma summable_of_summable_of_sub (hf : summable f) (h : ∀b, g b = 0 ∨ g b = f b) : summable g :=
id                                           └──────┘                         └──────┘ 
src                                          └──────┘                                 └──────┘
typ                                          └──────┘                         └──────┘ 
doc                                          └──────┘                                    └──────┘
538  (summable_iff_vanishing g).2 $
id    └────────────────────┘  
src   └────────────────────┘   
typ   └────────────────────┘  
539    assume e he,
id             └┘
typ            └┘
540    let ⟨s, hs⟩ := (summable_iff_vanishing f).1 hf e he in
id     └─┘    └┘      └────────────────────┘    └┘  └┘
src                    └────────────────────┘   
typ    └─┘    └┘      └────────────────────┘    └┘  └┘
541    ⟨s, assume t ht,
id                 └┘
typ                └┘
542      have eq : (t.filter (λb, g b = f b)).sum f = t.sum g :=
id                  └─────┘           └─┘    └──┘ 
src                  └─────┘                └─┘      └──┘
typ                 └─────┘           └─┘    └──┘ 
doc                  └─────┘
543        calc (t.filter (λb, g b = f b)).sum f = (t.filter (λb, g b = f b)).sum g :
id               └─────┘           └─┘      └─────┘           └─┘  
src               └─────┘                └─┘        └─────┘                └─┘
typ              └─────┘           └─┘      └─────┘           └─┘  
doc               └─────┘                            └─────┘
544            finset.sum_congr rfl (assume b hb, (finset.mem_filter.1 hb).2.symm)
id             └──────────────┘ └─┘          └┘   └───────────────┘  └┘  └──┘
src            └──────────────┘ └─┘                └───────────────┘      └──┘
typ            └──────────────┘ └─┘          └┘   └───────────────┘  └┘  └──┘
545          ... = t.sum g :
id                 └──┘ 
src                 └──┘
typ                └──┘ 
546          begin
st           └─────
547            refine finset.sum_subset (finset.filter_subset _) _,
id                    └───────────────┘  └──────────────────┘
src            └─────┘└───────────────┘ └──────────────────┘└───┘
typ            └─────┘└───────────────┘ └──────────────────┘└───┘
doc            └─────┘                                      └───┘
txt            └─────┘                                      └───┘
par            └─────┘                                      └───┘
pid                                                        └───┘
st   ────────────────────────────────────────────────────────────┘└─
548            assume b hbt hb,
src            └─────────────┘
typ            └─────────────┘
doc            └─────────────┘
txt            └─────────────┘
par            └─────────────┘
pid            └─────────────┘
st   ────────────────────────┘└─
549            simp only [(∉), finset.mem_filter, and_iff_right hbt] at hb,
id                            └───────────────┘  └───────────┘ └─┘
src            └─────────┘└──┘└───────────────┘└┘└───────────┘   └─────┘
typ            └─────────┘└──┘└───────────────┘└┘└───────────┘└─┘└─────┘
doc            └─────────┘ └──┘                 └┘                └─────┘
txt            └─────────┘ └──┘                 └┘                └─────┘
par            └─────────┘ └──┘                 └┘                └─────┘
pid                └──┘└┘ └──┘                 └┘                └───┘
st   ────────────────────────────────────────────────────────────────────┘└─
550            exact (h b).resolve_right hb
id                                     └┘
src            └────┘   └──────────────┘  
typ            └────┘ └──────────────┘└┘
doc            └────┘   └──────────────┘  
txt            └────┘   └──────────────┘  
par            └────┘   └──────────────┘  
pid                    └──────────────┘  
st   ───────────────────────────────────────
551          end,
src  ───────┘
typ  ───────┘
doc  ───────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘└─┘
552      eq ▸ hs _ $ finset.disjoint_of_subset_left (finset.filter_subset _) ht⟩
id       └┘         └────────────────────────────┘  └──────────────────┘    └┘
src      └┘         └────────────────────────────┘  └──────────────────┘
typ      └┘         └────────────────────────────┘  └──────────────────┘    └┘
553  
554  lemma summable_comp_of_summable_of_injective {i : γ → β} (hf : summable f) (hi : injective i) :
id                                                                └──────┘         └───────┘ 
src                                                                 └──────┘          └───────┘
typ                                                               └──────┘         └───────┘ 
doc                                                                 └──────┘
555    summable (f ∘ i) :=
id     └──────┘    
src    └──────┘    
typ    └──────┘    
doc    └──────┘
556  suffices summable (λb, if b ∈ set.range i then f b else 0),
id            └──────┘          └───────┘        
src           └──────┘            └───────┘
typ           └──────┘          └───────┘        
doc           └──────┘             └───────┘
557  begin
st   └─────
558    refine (summable_iff_summable_ne_zero_bij (λc _, i c) _ _ _).1 this,
id             └───────────────────────────────┘                     └──┘
src    └─────┘ └───────────────────────────────┘  └───┘  └─────────┘
typ    └─────┘ └───────────────────────────────┘  └───┘ └─────────┘└──┘
doc    └─────┘                                    └───┘  └─────────┘
txt    └─────┘                                    └───┘  └─────────┘
par    └─────┘                                    └───┘  └─────────┘
pid                                              └───┘  └─────────┘
st   ────────────────────────────────────────────────────────────────────┘└─
559    { assume c₁ c₂ hc₁ hc₂ eq, exact hi eq },
id                                      └┘ └┘
src      └─────────────────────┘  └────┘  └┘
typ      └─────────────────────┘  └────┘└┘└┘
doc      └─────────────────────┘  └────┘    
txt      └─────────────────────┘  └────┘    
par      └─────────────────────┘  └────┘    
pid      └─────────────────────┘           
st   ───┘└─────────────────────┘└────────────┘└┘
560    { assume b hb,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
561      split_ifs at hb,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid               └────┘
st   ──────────────────┘└─
562      { rcases h with ⟨c, rfl⟩,
id                
src        └─────┘ └────────────┘
typ        └─────┘└────────────┘
doc        └─────┘ └────────────┘
txt        └─────┘ └────────────┘
par        └─────┘ └────────────┘
pid               └────────────┘
st   ─────┘└────────────────────┘└─
563        exact ⟨c, hb, rfl⟩ },
id                  └┘  └─┘
src        └────┘  └┘  └┘└─┘└┘
typ        └────┘ └┘└┘└┘└─┘└┘
doc        └────┘  └┘  └┘   └┘
txt        └────┘  └┘  └┘   └┘
par        └────┘  └┘  └┘   └┘
pid               └┘  └┘   
st   ────────────────────────┘└┘
564      { contradiction } },
src        └────────────┘
typ        └────────────┘
doc        └────────────┘
txt        └────────────┘
par        └────────────┘
pid                     
st   ───────────────────┘└──┘
565    { assume c hc, exact if_pos (set.mem_range_self _) }
id                          └────┘  └────────────────┘
src      └─────────┘  └────┘└────┘ └────────────────┘└──┘
typ      └─────────┘  └────┘└────┘ └────────────────┘└──┘
doc      └─────────┘  └────┘                         └──┘
txt      └─────────┘  └────┘                         └──┘
par      └─────────┘  └────┘                         └──┘
pid      └─────────┘                                └─┘
st   ──────────────┘└────────────────────────────────────┘└─
566  end,
st   ──┘
567  summable_of_summable_of_sub _ _ hf $ assume b, by by_cases b ∈ set.range i; simp [h]
id   └─────────────────────────┘     └┘                          └───────┘         
src  └─────────────────────────┘                       └───────┘ └───────┘   └────┘ └─
typ  └─────────────────────────┘     └┘               └───────┘└───────┘  └────┘└─
doc                                                    └───────┘  └───────┘   └────┘ └─
txt                                                    └───────┘              └────┘ └─
par                                                    └───────┘              └────┘ └─
pid                                                                               
st                                                    └───────────────────────────────────
568  
src  
typ  
doc  
txt  
par  
pid  
st   
569  end uniform_group
570  
571  section cauchy_seq
572  open finset.Ico filter
573  
574  /-- If the extended distance between consequent points of a sequence is estimated
575  by a summable series of `nnreal`s, then the original sequence is a Cauchy sequence. -/
576  lemma cauchy_seq_of_edist_le_of_summable [emetric_space α] {f : ℕ → α} (d : ℕ → nnreal)
id                                             └───────────┘                     └────┘
src                                            └───────────┘                       └────┘
typ                                            └───────────┘                     └────┘
doc                                            └───────────┘                         └────┘
577    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f :=
id               └───┘       └───┘            └──────┘     └────────┘ 
src               └───┘           └───┘              └──────┘      └────────┘
typ              └───┘       └───┘            └──────┘     └────────┘ 
doc                                                   └──────┘      └────────┘
578  begin
st   └─────
579    refine emetric.cauchy_seq_iff_nnreal.2 (λ ε εpos, _),
id            └───────────────────────────┘
src    └─────┘└───────────────────────────┘└─┘  └─────────┘
typ    └─────┘└───────────────────────────┘└─┘  └─────────┘
doc    └─────┘└───────────────────────────┘└─┘  └─────────┘
txt    └─────┘                             └─┘  └─────────┘
par    └─────┘                             └─┘  └─────────┘
pid                                       └─┘  └─────────┘
st   ─────────────────────────────────────────────────────┘└─
580    -- Actually we need partial sums of `d` to be a Cauchy sequence
st   ──────────────────────────────────────────────────────────────────
581    replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) :=
id                  └────────┘             └─┘  └───┘    
src    └───────────┘└────────┘  └────┘ └─┘└─┘ └───┘ └┘ └────
typ    └───────────┘└────────┘  └────┘ └─┘└─┘ └───┘ └┘└────
doc    └───────────┘└────────┘  └────┘ └─┘    └───┘ └┘ └────
txt    └───────────┘            └────┘ └─┘          └┘ └────
par    └───────────┘            └────┘ └─┘          └┘ └────
pid           └─┘└─┘            └────┘ └─┘          └┘ └───
st   ──────────────────────────────────────────────────────────
582      let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ (tendsto_sum_nat_of_has_sum H),
id                    └┘    └────────────────────────┘    └────────────────────────┘
src  ───┘    └─┘ └───┘  └──┘└────────────────────────┘└─┘ └────────────────────────┘ 
typ  ───┘    └─┘└───┘└┘└──┘└────────────────────────┘└─┘ └────────────────────────┘ 
doc  ───┘    └─┘ └───┘  └──┘                          └─┘ └────────────────────────┘ 
txt  ───┘    └─┘ └───┘  └──┘                          └─┘                            
par  ───┘    └─┘ └───┘  └──┘                          └─┘                            
pid  ───┘    └─┘ └───┘  └──┘                          └─┘                            
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
583    -- Now we take the same `N` as in one of the definitions of a Cauchy sequence
st   ────────────────────────────────────────────────────────────────────────────────
584    refine (metric.cauchy_seq_iff'.1 hd ε (nnreal.coe_pos.2 εpos)).imp (λ N hN n hn, _),
id             └────────────────────┘   └┘   └────────────┘   └──┘
src    └─────┘ └────────────────────┘└─┘    └────────────┘└─┘    └─────┘  └────────────┘
typ    └─────┘ └────────────────────┘└─┘└┘ └────────────┘└─┘└──┘└─────┘  └────────────┘
doc    └─────┘ └────────────────────┘└─┘                  └─┘    └─────┘  └────────────┘
txt    └─────┘                       └─┘                  └─┘    └─────┘  └────────────┘
par    └─────┘                       └─┘                  └─┘    └─────┘  └────────────┘
pid                                 └─┘                  └─┘    └─────┘  └────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
585    have hsum := hN n hn,
id                  └┘  └┘
src    └───────────┘   
typ    └───────────┘└┘└┘
doc    └───────────┘   
txt    └───────────┘   
par    └───────────┘   
pid    └───────┘└─┘   
st   ─────────────────────┘└─
586    -- We simplify the known inequality
st   ──────────────────────────────────────
587    rw [dist_nndist, nnreal.nndist_eq, ← sum_range_add_sum_Ico _ hn, nnreal.add_sub_cancel'] at hsum,
id         └─────────┘  └──────────────┘    └───────────────────┘   └┘  └────────────────────┘
src    └──┘└─────────┘└┘└──────────────┘└──┘└───────────────────┘└─┘  └┘└────────────────────┘└───────┘
typ    └──┘└─────────┘└┘└──────────────┘└──┘└───────────────────┘└─┘└┘└┘└────────────────────┘└───────┘
doc    └──┘└─────────┘└┘                └──┘                     └─┘  └┘                      └───────┘
txt    └──┘           └┘                └──┘                     └─┘  └┘                      └───────┘
par    └──┘           └┘                └──┘                     └─┘  └┘                      └───────┘
pid      └┘           └┘                └──┘                     └─┘  └┘                      └──────┘
st   ────────────────┘└────────────────┘└────────────────────────────┘└──────────────────────┘└──────┘└─
588    norm_cast at hsum,
src    └───────────────┘
typ    └───────────────┘
doc    └───────────────┘
txt    └───────────────┘
par    └───────────────┘
pid             └──────┘
st   ──────────────────┘└─
589    replace hsum := lt_of_le_of_lt (le_max_left _ _) hsum,
id                     └────────────┘  └─────────┘      └──┘
src    └──────────────┘└────────────┘ └─────────┘└────┘
typ    └──────────────┘└────────────┘ └─────────┘└────┘└──┘
doc    └──────────────┘                          └────┘
txt    └──────────────┘                          └────┘
par    └──────────────┘                          └────┘
pid           └───┘└─┘                          └────┘
st   ──────────────────────────────────────────────────────┘└─
590  
st   
591    -- Then use `hf` to simplify the goal to the same form
st   ─────────────────────────────────────────────────────────
592    apply lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn (λ k _ _, hf k)),
id           └────────────┘  └──────────────────────────┘ └┘           └┘
src    └────┘└────────────┘ └──────────────────────────┘    └──────┘   └┘
typ    └────┘└────────────┘ └──────────────────────────┘└┘  └──────┘└┘ └┘
doc    └────┘               └──────────────────────────┘    └──────┘   └┘
txt    └────┘                                               └──────┘   └┘
par    └────┘                                               └──────┘   └┘
pid                                                        └──────┘   └┘
st   ───────────────────────────────────────────────────────────────────────┘└─
593    assumption_mod_cast
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid                       
st   ─────────────────────┘
594  end
st   └─┘
595  
596  /-- If the distance between consequent points of a sequence is estimated by a summable series,
597  then the original sequence is a Cauchy sequence. -/
598  lemma cauchy_seq_of_dist_le_of_summable [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
id                                            └──────────┘                     
src                                           └──────────┘                       
typ                                           └──────────┘                     
doc                                           └──────────┘
599    (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f :=
id               └──┘       └───┘            └──────┘     └────────┘ 
src               └──┘           └───┘              └──────┘      └────────┘
typ              └──┘       └───┘            └──────┘     └────────┘ 
doc                                                  └──────┘      └────────┘
600  begin
st   └─────
601    refine metric.cauchy_seq_iff'.2 (λε εpos, _),
id            └────────────────────┘
src    └─────┘└────────────────────┘└─┘  └────────┘
typ    └─────┘└────────────────────┘└─┘  └────────┘
doc    └─────┘└────────────────────┘└─┘  └────────┘
txt    └─────┘                      └─┘  └────────┘
par    └─────┘                      └─┘  └────────┘
pid                                └─┘  └────────┘
st   ─────────────────────────────────────────────┘└─
602    replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) :=
id                  └────────┘             └─┘  └───┘    
src    └───────────┘└────────┘  └────┘ └─┘└─┘ └───┘ └┘ └────
typ    └───────────┘└────────┘  └────┘ └─┘└─┘ └───┘ └┘└────
doc    └───────────┘└────────┘  └────┘ └─┘    └───┘ └┘ └────
txt    └───────────┘            └────┘ └─┘          └┘ └────
par    └───────────┘            └────┘ └─┘          └┘ └────
pid           └─┘└─┘            └────┘ └─┘          └┘ └───
st   ──────────────────────────────────────────────────────────
603      let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ (tendsto_sum_nat_of_has_sum H),
id                    └┘    └────────────────────────┘    └────────────────────────┘
src  ───┘    └─┘ └───┘  └──┘└────────────────────────┘└─┘ └────────────────────────┘ 
typ  ───┘    └─┘└───┘└┘└──┘└────────────────────────┘└─┘ └────────────────────────┘ 
doc  ───┘    └─┘ └───┘  └──┘                          └─┘ └────────────────────────┘ 
txt  ───┘    └─┘ └───┘  └──┘                          └─┘                            
par  ───┘    └─┘ └───┘  └──┘                          └─┘                            
pid  ───┘    └─┘ └───┘  └──┘                          └─┘                            
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
604    refine (metric.cauchy_seq_iff'.1 hd ε εpos).imp (λ N hN n hn, _),
id             └────────────────────┘   └┘  └──┘
src    └─────┘ └────────────────────┘└─┘       └────┘  └────────────┘
typ    └─────┘ └────────────────────┘└─┘└┘└──┘└────┘  └────────────┘
doc    └─────┘ └────────────────────┘└─┘       └────┘  └────────────┘
txt    └─────┘                       └─┘       └────┘  └────────────┘
par    └─────┘                       └─┘       └────┘  └────────────┘
pid                                 └─┘       └────┘  └────────────┘
st   ─────────────────────────────────────────────────────────────────┘└─
605    have hsum := hN n hn,
id                  └┘  └┘
src    └───────────┘   
typ    └───────────┘└┘└┘
doc    └───────────┘   
txt    └───────────┘   
par    └───────────┘   
pid    └───────┘└─┘   
st   ─────────────────────┘└─
606    rw [real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum,
id         └──────────┘    └────────────┘   └┘
src    └──┘└──────────┘└──┘└────────────┘└─┘  └───────┘
typ    └──┘└──────────┘└──┘└────────────┘└─┘└┘└───────┘
doc    └──┘            └──┘              └─┘  └───────┘
txt    └──┘            └──┘              └─┘  └───────┘
par    └──┘            └──┘              └─┘  └───────┘
pid      └┘            └──┘              └─┘  └──────┘
st   ─────────────────┘└─────────────────────┘└──────┘└─
607    calc dist (f n) (f N) = dist (f N) (f n) : dist_comm _ _
id     └──┘                    └──┘            └───────┘
src    └──┘                    └──┘               └───────┘
typ    └──┘                    └──┘            └───────┘
doc    └──┘
st   ───────────────────────────────────────────────────────────
608    ... ≤ (Ico N n).sum d : dist_le_Ico_sum_of_dist_le hn (λ k _ _, hf k)
id            └─┘             └────────────────────────┘ └┘        └┘
src           └─┘              └────────────────────────┘
typ           └─┘             └────────────────────────┘ └┘        └┘
doc           └─┘              └────────────────────────┘
st   ────────────────────────────────────────────────────────────────────────
609    ... ≤ abs ((Ico N n).sum d) : le_abs_self _
id           └─┘           └─┘       └─────────┘
src          └─┘           └─┘       └─────────┘
typ          └─┘           └─┘       └─────────┘
st   ──────────────────────────────────────────────
610    ... < ε : hsum
id              └──┘
typ             └──┘
st   ───────────────┘
611  end
st   ──┘
612  
613  lemma cauchy_seq_of_summable_dist [metric_space α] {f : ℕ → α}
id                                      └──────────┘           
src                                     └──────────┘         
typ                                     └──────────┘           
doc                                     └──────────┘
614    (h : summable (λn, dist (f n) (f n.succ))) : cauchy_seq f :=
id          └──────┘     └──┘       └───┘      └────────┘ 
src         └──────┘      └──┘           └───┘      └────────┘
typ         └──────┘     └──┘       └───┘      └────────┘ 
doc         └──────┘                                └────────┘
615  cauchy_seq_of_dist_le_of_summable _ (λ _, le_refl _) h
id   └───────────────────────────────┘        └─────┘    
src  └───────────────────────────────┘         └─────┘
typ  └───────────────────────────────┘        └─────┘    
doc  └───────────────────────────────┘
616  
617  lemma dist_le_tsum_of_dist_le_of_tendsto [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
id                                             └──────────┘                     
src                                            └──────────┘                       
typ                                            └──────────┘                     
doc                                            └──────────┘
618    (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a))
id               └──┘       └───┘            └──────┘                └─────┘  └────┘   
src               └──┘           └───┘              └──────┘                  └─────┘   └────┘  
typ              └──┘       └───┘            └──────┘                └─────┘  └────┘   
doc                                                  └──────┘                  └─────┘   └────┘  
619    (n : ℕ) :
id          
src         
typ         
620    dist (f n) a ≤ ∑ m, d (n + m) :=
id     └──┘             
src    └──┘                  
typ    └──┘             
doc                     
621  begin
st   └─────
622    refine le_of_tendsto at_top_ne_bot (tendsto_dist tendsto_const_nhds ha)
id            └───────────┘ └───────────┘  └──────────┘ └────────────────┘ └┘
src    └─────┘└───────────┘└───────────┘ └──────────┘└────────────────┘  └─
typ    └─────┘└───────────┘└───────────┘ └──────────┘└────────────────┘└┘└─
doc    └─────┘                                                           └─
txt    └─────┘                                                           └─
par    └─────┘                                                           └─
pid                                                                     └─
st   ──────────────────────────────────────────────────────────────────────────
623      (mem_at_top_sets.2 ⟨n, λ m hnm, _⟩),
id        └─────────────┘    
src  ───┘ └─────────────┘└─┘  └┘ └─────────┘
typ  ───┘ └─────────────┘└─┘ └┘ └─────────┘
doc  ───┘                └─┘  └┘ └─────────┘
txt  ───┘                └─┘  └┘ └─────────┘
par  ───┘                └─┘  └┘ └─────────┘
pid  ───┘                └─┘  └┘ └─────────┘
st   ──────────────────────────────────────┘└─
624    refine le_trans (dist_le_Ico_sum_of_dist_le hnm (λ k _ _, hf k)) _,
id            └──────┘  └────────────────────────┘ └─┘           └┘
src    └─────┘└──────┘ └────────────────────────┘     └──────┘   └──┘
typ    └─────┘└──────┘ └────────────────────────┘└─┘  └──────┘└┘ └──┘
doc    └─────┘         └────────────────────────┘     └──────┘   └──┘
txt    └─────┘                                        └──────┘   └──┘
par    └─────┘                                        └──────┘   └──┘
pid                                                  └──────┘   └──┘
st   ───────────────────────────────────────────────────────────────────┘└─
625    rw [sum_Ico_eq_sum_range],
id         └──────────────────┘
src    └──┘└──────────────────┘
typ    └──┘└──────────────────┘
doc    └──┘                    
txt    └──┘                    
par    └──┘                    
pid      └┘                    
st   ─────────────────────────┘└──
626    refine sum_le_tsum (range _) (λ _ _, le_trans dist_nonneg (hf _)) _,
id            └─────────┘  └───┘            └──────┘ └─────────┘  └┘
src    └─────┘└─────────┘ └───┘└──┘  └────┘└──────┘└─────────┘   └────┘
typ    └─────┘└─────────┘ └───┘└──┘  └────┘└──────┘└─────────┘ └┘└────┘
doc    └─────┘            └───┘└──┘  └────┘                      └────┘
txt    └─────┘                 └──┘  └────┘                      └────┘
par    └─────┘                 └──┘  └────┘                      └────┘
pid                           └──┘  └────┘                      └────┘
st   ────────────────────────────────────────────────────────────────────┘└─
627    exact summable_comp_of_summable_of_injective _ hd (add_left_injective n)
id           └────────────────────────────────────┘   └┘  └────────────────┘ 
src    └────┘└────────────────────────────────────┘└─┘   └────────────────┘ └┘
typ    └────┘└────────────────────────────────────┘└─┘└┘ └────────────────┘└┘
doc    └────┘                                      └─┘                      └┘
txt    └────┘                                      └─┘                      └┘
par    └────┘                                      └─┘                      └┘
pid                                               └─┘                      
st   ──────────────────────────────────────────────────────────────────────────┘
628  end
st   └─┘
629  
630  lemma dist_le_tsum_of_dist_le_of_tendsto₀ [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
id                                              └──────────┘                     
src                                             └──────────┘                       
typ                                             └──────────┘                     
doc                                             └──────────┘
631    (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a)) :
id               └──┘       └───┘            └──────┘                └─────┘  └────┘   
src               └──┘           └───┘              └──────┘                  └─────┘   └────┘  
typ              └──┘       └───┘            └──────┘                └─────┘  └────┘   
doc                                                  └──────┘                  └─────┘   └────┘  
632    dist (f 0) a ≤ tsum d :=
id     └──┘        └──┘ 
src    └──┘          └──┘
typ    └──┘        └──┘ 
doc                   └──┘
633  by simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0
id                  └──────┘        └────────────────────────────────┘  └┘ └┘ └┘
src     └──────────┘└──────┘└──────┘└────────────────────────────────┘       └──
typ     └──────────┘└──────┘└──────┘└────────────────────────────────┘└┘└┘└┘└──
doc     └──────────┘        └──────┘                                         └──
txt     └──────────┘        └──────┘                                         └──
par     └──────────┘        └──────┘                                         └──
pid          └──┘└┘        └────┘                                         └─
st     └────────────────────────────────────────────────────────────────────────────
634  
src  
typ  
doc  
txt  
par  
pid  
st   
635  lemma dist_le_tsum_dist_of_tendsto [metric_space α] {f : ℕ → α}
id                                       └──────────┘           
src                                      └──────────┘         
typ                                      └──────────┘           
doc                                      └──────────┘
636    (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) (n) :
id          └──────┘     └──┘       └───┘                 └─────┘  └────┘   
src         └──────┘      └──┘           └───┘                  └─────┘   └────┘  
typ         └──────┘     └──┘       └───┘                 └─────┘  └────┘   
doc         └──────┘                                            └─────┘   └────┘  
637    dist (f n) a ≤ ∑ m, dist (f (n+m)) (f (n+m).succ) :=
id     └──┘         └──┘           └──┘
src    └──┘             └──┘                 └──┘
typ    └──┘         └──┘           └──┘
doc                     
638  show dist (f n) a ≤ ∑ m, (λx, dist (f x) (f x.succ)) (n + m), from
id        └──┘             └──┘       └───┘      
src       └──┘                  └──┘           └───┘      
typ       └──┘             └──┘       └───┘      
doc                        
639  dist_le_tsum_of_dist_le_of_tendsto (λ n, dist (f n) (f n.succ)) (λ _, le_refl _) h ha n
id   └────────────────────────────────┘      └──┘       └───┘        └─────┘     └┘ 
src  └────────────────────────────────┘       └──┘           └───┘         └─────┘
typ  └────────────────────────────────┘      └──┘       └───┘        └─────┘     └┘ 
640  
641  lemma dist_le_tsum_dist_of_tendsto₀ [metric_space α] {f : ℕ → α}
id                                        └──────────┘           
src                                       └──────────┘         
typ                                       └──────────┘           
doc                                       └──────────┘
642    (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) :
id          └──────┘     └──┘       └───┘                 └─────┘  └────┘   
src         └──────┘      └──┘           └───┘                  └─────┘   └────┘  
typ         └──────┘     └──┘       └───┘                 └─────┘  └────┘   
doc         └──────┘                                            └─────┘   └────┘  
643    dist (f 0) a ≤ ∑ n, dist (f n) (f n.succ) :=
id     └──┘          └──┘       └───┘
src    └──┘             └──┘           └───┘
typ    └──┘          └──┘       └───┘
doc                     
644  by simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0
id                  └──────┘        └──────────────────────────┘  └┘
src     └──────────┘└──────┘└──────┘└──────────────────────────┘   └──
typ     └──────────┘└──────┘└──────┘└──────────────────────────┘└┘└──
doc     └──────────┘        └──────┘                               └──
txt     └──────────┘        └──────┘                               └──
par     └──────────┘        └──────┘                               └──
pid          └──┘└┘        └────┘                               └─
st     └────────────────────────────────────────────────────────────────
645  
src  
typ  
doc  
txt  
par  
pid  
st   
646  end cauchy_seq